The dog chases the squirrel. The dog is green. The dog is red. The dog needs the squirrel. The squirrel chases the dog. The squirrel is green. The squirrel is red. The squirrel is young. The squirrel likes the dog. The squirrel needs the dog. If something chases the squirrel then it chases the dog. If something chases the dog and it needs the dog then the dog needs the squirrel. If the squirrel needs the dog then the squirrel is big. If something likes the squirrel and the squirrel likes the dog then it chases the squirrel. If something likes the squirrel and the squirrel is big then it needs the dog. If something is big then it likes the squirrel. If the squirrel is big then the squirrel is red. If the squirrel chases the dog then the squirrel is red.
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is red.
("dog" "is" "red" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
If something chases the squirrel then it chases the dog.
((("something" "chases" "squirrel" "+")) -> ("something" "chases" "dog" "+"))
If something chases the dog and it needs the dog then the dog needs the squirrel.
((("something" "chases" "dog" "+") ("something" "needs" "dog" "+")) -> ("dog" "needs" "squirrel" "+"))
If the squirrel needs the dog then the squirrel is big.
((("squirrel" "needs" "dog" "+")) -> ("squirrel" "is" "big" "+"))
If something likes the squirrel and the squirrel likes the dog then it chases the squirrel.
((("something" "likes" "squirrel" "+") ("squirrel" "likes" "dog" "+")) -> ("something" "chases" "squirrel" "+"))
If something likes the squirrel and the squirrel is big then it needs the dog.
((("something" "likes" "squirrel" "+") ("squirrel" "is" "big" "+")) -> ("something" "needs" "dog" "+"))
If something is big then it likes the squirrel.
((("something" "is" "big" "+")) -> ("something" "likes" "squirrel" "+"))
If the squirrel is big then the squirrel is red.
((("squirrel" "is" "big" "+")) -> ("squirrel" "is" "red" "+"))
If the squirrel chases the dog then the squirrel is red.
((("squirrel" "chases" "dog" "+")) -> ("squirrel" "is" "red" "+"))
The dog needs the squirrel.
True
1
proof
[(triple4 OR ((triple5 triple10) -> rule2) OR ((((((((((triple10) -> rule3)) -> rule6) triple9) -> rule4)) -> rule1) triple10) -> rule2))]
("dog" "needs" "squirrel" "+")
triple4
((triple5 triple10) -> (rule2 % int1))
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int1
((((((((((triple10) -> (rule3 % int5))) -> (rule6 % int4)) triple9) -> (rule4 % int3))) -> (rule1 % int2)) triple10) -> (rule2 % int1))
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int4
The squirrel is big.
("squirrel" "is" "big" "+")
int5
The dog does not need the squirrel.
False
1
inv-proof
[(triple4 OR ((triple5 triple10) -> rule2) OR ((((((((((triple10) -> rule3)) -> rule6) triple9) -> rule4)) -> rule1) triple10) -> rule2))]
("dog" "needs" "squirrel" "-")
triple4
((triple5 triple10) -> (rule2 % int1))
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int1
((((((((((triple10) -> (rule3 % int5))) -> (rule6 % int4)) triple9) -> (rule4 % int3))) -> (rule1 % int2)) triple10) -> (rule2 % int1))
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int4
The squirrel is big.
("squirrel" "is" "big" "+")
int5
The squirrel is big.
True
2
proof
[(((triple10) -> rule3))]
("squirrel" "is" "big" "+")
((triple10) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The dog does not chase the dog.
False
2
inv-proof
[(((triple1) -> rule1))]
("dog" "chases" "dog" "-")
((triple1) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The squirrel likes the squirrel.
True
3
proof
[(((((triple10) -> rule3)) -> rule6))]
("squirrel" "likes" "squirrel" "+")
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel does not like the squirrel.
False
3
inv-proof
[(((((triple10) -> rule3)) -> rule6))]
("squirrel" "likes" "squirrel" "-")
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The dog does not need the dog.
Unknown
inv-rconc
[@2: The dog needs the dog.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("dog" "needs" "dog" "-")
The dog likes the squirrel.
Unknown
rconc
[@1: The dog likes the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "likes" "squirrel" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
@0: The dog chases the squirrel.[(triple1)] The dog is green.[(triple2)] The dog is red.[(triple3)] The dog needs the squirrel.[(triple4 OR ((triple5 triple10) -> rule2) OR ((((((((((triple10) -> rule3)) -> rule6) triple9) -> rule4)) -> rule1) triple10) -> rule2))] The squirrel chases the dog.[(triple5 OR ((((((((triple10) -> rule3)) -> rule6) triple9) -> rule4)) -> rule1))] The squirrel is green.[(triple6)] The squirrel is red.[(triple7 OR ((triple5) -> rule8) OR ((((triple10) -> rule3)) -> rule7) OR ((((((((((triple10) -> rule3)) -> rule6) triple9) -> rule4)) -> rule1)) -> rule8))] The squirrel is young.[(triple8)] The squirrel likes the dog.[(triple9)] The squirrel needs the dog.[(triple10)] @1: The dog chases the dog.[(((triple1) -> rule1))] The squirrel is big.[(((triple10) -> rule3))] @2: The squirrel likes the squirrel.[(((((triple10) -> rule3)) -> rule6))] @3: The squirrel chases the squirrel.[(((((((triple10) -> rule3)) -> rule6) triple9) -> rule4))]
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is red.
("dog" "is" "red" "+")
triple3
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple4
((triple5 triple10) -> (rule2 % int1))
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int1
((((((((((triple10) -> (rule3 % int5))) -> (rule6 % int4)) triple9) -> (rule4 % int3))) -> (rule1 % int2)) triple10) -> (rule2 % int1))
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int4
The squirrel is big.
("squirrel" "is" "big" "+")
int5
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple5
((((((((triple10) -> (rule3 % int4))) -> (rule6 % int3)) triple9) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int3
The squirrel is big.
("squirrel" "is" "big" "+")
int4
The squirrel is green.
("squirrel" "is" "green" "+")
triple6
The squirrel is red.
("squirrel" "is" "red" "+")
triple7
((triple5) -> (rule8 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
((((((((((triple10) -> (rule3 % int5))) -> (rule6 % int4)) triple9) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int4
The squirrel is big.
("squirrel" "is" "big" "+")
int5
The squirrel is young.
("squirrel" "is" "young" "+")
triple8
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple9
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple10
The dog chases the dog.
("dog" "chases" "dog" "+")
((triple1) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((triple10) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((((((triple10) -> (rule3 % int3))) -> (rule6 % int2)) triple9) -> (rule4 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3