The dog eats the squirrel. The dog is big. The dog is cold. The dog is kind. The dog is red. The dog is rough. The dog likes the squirrel. The dog needs the squirrel. The squirrel eats the dog. The squirrel is not big. The squirrel is cold. The squirrel is kind. The squirrel is red. The squirrel is rough. The squirrel likes the dog. The squirrel needs the dog. If the squirrel eats the dog then the dog eats the squirrel. If the squirrel likes the dog and the dog needs the squirrel then the dog eats the squirrel. If something eats the squirrel and the squirrel is rough then the squirrel needs the dog. If something needs the squirrel then the squirrel needs the dog. If something likes the dog and the dog needs the squirrel then the squirrel needs the dog. If something likes the dog then it needs the squirrel. If something eats the dog and the dog likes the squirrel then it needs the dog. If something eats the squirrel then it eats the dog.
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
The squirrel is not big.
("squirrel" "is" "big" "-")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
If the squirrel eats the dog then the dog eats the squirrel.
((("squirrel" "eats" "dog" "+")) -> ("dog" "eats" "squirrel" "+"))
If the squirrel likes the dog and the dog needs the squirrel then the dog eats the squirrel.
((("squirrel" "likes" "dog" "+") ("dog" "needs" "squirrel" "+")) -> ("dog" "eats" "squirrel" "+"))
If something eats the squirrel and the squirrel is rough then the squirrel needs the dog.
((("something" "eats" "squirrel" "+") ("squirrel" "is" "rough" "+")) -> ("squirrel" "needs" "dog" "+"))
If something needs the squirrel then the squirrel needs the dog.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "needs" "dog" "+"))
If something likes the dog and the dog needs the squirrel then the squirrel needs the dog.
((("something" "likes" "dog" "+") ("dog" "needs" "squirrel" "+")) -> ("squirrel" "needs" "dog" "+"))
If something likes the dog then it needs the squirrel.
((("something" "likes" "dog" "+")) -> ("something" "needs" "squirrel" "+"))
If something eats the dog and the dog likes the squirrel then it needs the dog.
((("something" "eats" "dog" "+") ("dog" "likes" "squirrel" "+")) -> ("something" "needs" "dog" "+"))
If something eats the squirrel then it eats the dog.
((("something" "eats" "squirrel" "+")) -> ("something" "eats" "dog" "+"))
The squirrel is kind.
True
1
proof
[(triple12)]
("squirrel" "is" "kind" "+")
triple12
The dog does not eat the squirrel.
False
1
inv-proof
[(triple1 OR ((triple9) -> rule1) OR ((triple15 triple8) -> rule2))]
("dog" "eats" "squirrel" "-")
triple1
((triple9) -> (rule1 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
((triple15 triple8) -> (rule2 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The squirrel needs the squirrel.
True
2
proof
[(((triple15) -> rule6))]
("squirrel" "needs" "squirrel" "+")
((triple15) -> (rule6 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The dog does not eat the dog.
False
2
inv-proof
[(((triple1) -> rule8) OR ((((triple9) -> rule1)) -> rule8) OR ((((triple15 triple8) -> rule2)) -> rule8))]
("dog" "eats" "dog" "-")
((triple1) -> (rule8 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule8 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int2
((((triple15 triple8) -> (rule2 % int2))) -> (rule8 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int2
The dog needs the dog.
True
4
proof
[(((((triple1) -> rule8) triple7) -> rule7) OR ((((((triple9) -> rule1)) -> rule8) triple7) -> rule7) OR ((((((triple15 triple8) -> rule2)) -> rule8) triple7) -> rule7))]
("dog" "needs" "dog" "+")
((((triple1) -> (rule8 % int2)) triple7) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
((((((triple9) -> (rule1 % int3))) -> (rule8 % int2)) triple7) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int3
((((((triple15 triple8) -> (rule2 % int3))) -> (rule8 % int2)) triple7) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int3
The dog does not need the dog.
False
4
inv-proof
[(((((triple1) -> rule8) triple7) -> rule7) OR ((((((triple9) -> rule1)) -> rule8) triple7) -> rule7) OR ((((((triple15 triple8) -> rule2)) -> rule8) triple7) -> rule7))]
("dog" "needs" "dog" "-")
((((triple1) -> (rule8 % int2)) triple7) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
((((((triple9) -> (rule1 % int3))) -> (rule8 % int2)) triple7) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int3
((((((triple15 triple8) -> (rule2 % int3))) -> (rule8 % int2)) triple7) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int3
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 squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The dog eats the squirrel.[(triple1 OR ((triple9) -> rule1) OR ((triple15 triple8) -> rule2))] The dog is big.[(triple2)] The dog is cold.[(triple3)] The dog is kind.[(triple4)] The dog is red.[(triple5)] The dog is rough.[(triple6)] The dog likes the squirrel.[(triple7)] The dog needs the squirrel.[(triple8)] The squirrel eats the dog.[(triple9)] The squirrel is cold.[(triple11)] The squirrel is kind.[(triple12)] The squirrel is not big.[(triple10)] The squirrel is red.[(triple13)] The squirrel is rough.[(triple14)] The squirrel likes the dog.[(triple15)] The squirrel needs the dog.[(triple16 OR ((triple8) -> rule4) OR ((triple1 triple14) -> rule3) OR ((triple15 triple8) -> rule5) OR ((triple9 triple7) -> rule7) OR ((((triple15) -> rule6)) -> rule4) OR ((((triple9) -> rule1) triple14) -> rule3) OR ((((triple15 triple8) -> rule2) triple14) -> rule3))] @1: The dog eats the dog.[(((triple1) -> rule8) OR ((((triple9) -> rule1)) -> rule8) OR ((((triple15 triple8) -> rule2)) -> rule8))] The squirrel needs the squirrel.[(((triple15) -> rule6))] @2: The dog needs the dog.[(((((triple1) -> rule8) triple7) -> rule7) OR ((((((triple9) -> rule1)) -> rule8) triple7) -> rule7) OR ((((((triple15 triple8) -> rule2)) -> rule8) triple7) -> rule7))]
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple1
((triple9) -> (rule1 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
((triple15 triple8) -> (rule2 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The dog is red.
("dog" "is" "red" "+")
triple5
The dog is rough.
("dog" "is" "rough" "+")
triple6
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple7
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple8
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple9
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple11
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple12
The squirrel is not big.
("squirrel" "is" "big" "-")
triple10
The squirrel is red.
("squirrel" "is" "red" "+")
triple13
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple14
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple15
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple16
((triple8) -> (rule4 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
((triple1 triple14) -> (rule3 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
((triple15 triple8) -> (rule5 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
((triple9 triple7) -> (rule7 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
((((triple15) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
((((triple9) -> (rule1 % int2)) triple14) -> (rule3 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int2
((((triple15 triple8) -> (rule2 % int2)) triple14) -> (rule3 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
((triple1) -> (rule8 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule8 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int2
((((triple15 triple8) -> (rule2 % int2))) -> (rule8 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((triple15) -> (rule6 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
((((triple1) -> (rule8 % int2)) triple7) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
((((((triple9) -> (rule1 % int3))) -> (rule8 % int2)) triple7) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int3
((((((triple15 triple8) -> (rule2 % int3))) -> (rule8 % int2)) triple7) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int3