The dog eats the squirrel. The dog is red. The dog is young. The dog sees the squirrel. The squirrel eats the dog. The squirrel is round. The squirrel sees the dog. If someone visits the dog and they see the squirrel then they visit the squirrel. If someone visits the squirrel then the squirrel visits the dog. If someone eats the squirrel and the squirrel visits the dog then the squirrel is kind. If someone eats the dog then the dog is big. If someone visits the squirrel and they eat the dog then they visit the dog. If someone sees the dog then the dog eats the squirrel. If someone is red and they visit the dog then the dog sees the squirrel. If someone is young then they visit the squirrel.
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is young.
("dog" "is" "young" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
If someone visits the dog and they see the squirrel then they visit the squirrel.
((("someone" "visits" "dog" "+") ("someone" "sees" "squirrel" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone visits the squirrel then the squirrel visits the dog.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "visits" "dog" "+"))
If someone eats the squirrel and the squirrel visits the dog then the squirrel is kind.
((("someone" "eats" "squirrel" "+") ("squirrel" "visits" "dog" "+")) -> ("squirrel" "is" "kind" "+"))
If someone eats the dog then the dog is big.
((("someone" "eats" "dog" "+")) -> ("dog" "is" "big" "+"))
If someone visits the squirrel and they eat the dog then they visit the dog.
((("someone" "visits" "squirrel" "+") ("someone" "eats" "dog" "+")) -> ("someone" "visits" "dog" "+"))
If someone sees the dog then the dog eats the squirrel.
((("someone" "sees" "dog" "+")) -> ("dog" "eats" "squirrel" "+"))
If someone is red and they visit the dog then the dog sees the squirrel.
((("someone" "is" "red" "+") ("someone" "visits" "dog" "+")) -> ("dog" "sees" "squirrel" "+"))
If someone is young then they visit the squirrel.
((("someone" "is" "young" "+")) -> ("someone" "visits" "squirrel" "+"))
The squirrel eats the dog.
True
1
proof
[(triple5)]
("squirrel" "eats" "dog" "+")
triple5
The dog does not see the squirrel.
False
1
inv-proof
[(triple4)]
("dog" "sees" "squirrel" "-")
triple4
The dog visits the squirrel.
True
2
proof
[(((triple3) -> rule8))]
("dog" "visits" "squirrel" "+")
((triple3) -> (rule8 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The dog is not big.
False
2
inv-proof
[(((triple5) -> rule4))]
("dog" "is" "big" "-")
((triple5) -> (rule4 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The squirrel visits the dog.
True
3
proof
[(((((triple3) -> rule8)) -> rule2))]
("squirrel" "visits" "dog" "+")
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
The squirrel does not visit the dog.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule2))]
("squirrel" "visits" "dog" "-")
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
The squirrel is kind.
True
5
proof
[(((triple1 ((((triple3) -> rule8)) -> rule2)) -> rule3) OR ((((triple7) -> rule6) ((((triple3) -> rule8)) -> rule2)) -> rule3))]
("squirrel" "is" "kind" "+")
((triple1 ((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int3
((((triple7) -> (rule6 % int4)) ((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int3
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int4
The squirrel is not kind.
False
5
inv-proof
[(((triple1 ((((triple3) -> rule8)) -> rule2)) -> rule3) OR ((((triple7) -> rule6) ((((triple3) -> rule8)) -> rule2)) -> rule3))]
("squirrel" "is" "kind" "-")
((triple1 ((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int3
((((triple7) -> (rule6 % int4)) ((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int3
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int4
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The dog visits the dog.
Unknown
rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "visits" "dog" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
The squirrel is not red.
Unknown
inv-random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The dog eats the squirrel.[(triple1 OR ((triple7) -> rule6))] The dog is red.[(triple2)] The dog is young.[(triple3)] The dog sees the squirrel.[(triple4)] The squirrel eats the dog.[(triple5)] The squirrel is round.[(triple6)] The squirrel sees the dog.[(triple7)] @1: The dog is big.[(((triple5) -> rule4))] The dog visits the squirrel.[(((triple3) -> rule8))] @2: The squirrel visits the dog.[(((((triple3) -> rule8)) -> rule2))] @3: The squirrel is kind.[(((triple1 ((((triple3) -> rule8)) -> rule2)) -> rule3) OR ((((triple7) -> rule6) ((((triple3) -> rule8)) -> rule2)) -> rule3))]
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple1
((triple7) -> (rule6 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The dog is red.
("dog" "is" "red" "+")
triple2
The dog is young.
("dog" "is" "young" "+")
triple3
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple4
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple5
The squirrel is round.
("squirrel" "is" "round" "+")
triple6
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple7
The dog is big.
("dog" "is" "big" "+")
((triple5) -> (rule4 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
((triple3) -> (rule8 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple1 ((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int3
((((triple7) -> (rule6 % int4)) ((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int3
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int4