The dog is big. The dog is cold. The dog is green. The dog is red. The dog is young. The dog needs the squirrel. The dog sees the squirrel. The dog visits the squirrel. The squirrel is big. The squirrel is cold. The squirrel is green. The squirrel is red. The squirrel is young. The squirrel needs the dog. The squirrel sees the dog. The squirrel visits the dog. If something is big and red then it needs the squirrel. If the squirrel sees the dog and the squirrel needs the dog then the squirrel visits the dog. If something is young then it is green. If something is green then it is cold. If something sees the dog and it visits the squirrel then the squirrel sees the dog. If something is cold then it visits the squirrel.
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If something is big and red then it needs the squirrel.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "needs" "squirrel" "+"))
If the squirrel sees the dog and the squirrel needs the dog then the squirrel visits the dog.
((("squirrel" "sees" "dog" "+") ("squirrel" "needs" "dog" "+")) -> ("squirrel" "visits" "dog" "+"))
If something is young then it is green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something sees the dog and it visits the squirrel then the squirrel sees the dog.
((("something" "sees" "dog" "+") ("something" "visits" "squirrel" "+")) -> ("squirrel" "sees" "dog" "+"))
If something is cold then it visits the squirrel.
((("something" "is" "cold" "+")) -> ("something" "visits" "squirrel" "+"))
The dog sees the squirrel.
True
1
proof
[(triple7)]
("dog" "sees" "squirrel" "+")
triple7
The squirrel does not visit the dog.
False
1
inv-proof
[(triple16 OR ((triple15 triple14) -> rule2))]
("squirrel" "visits" "dog" "-")
triple16
((triple15 triple14) -> (rule2 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The dog is big.[(triple1)] The dog is cold.[(triple2 OR ((triple3) -> rule4) OR ((((triple5) -> rule3)) -> rule4))] The dog is green.[(triple3 OR ((triple5) -> rule3))] The dog is red.[(triple4)] The dog is young.[(triple5)] The dog needs the squirrel.[(triple6 OR ((triple1 triple4) -> rule1))] The dog sees the squirrel.[(triple7)] The dog visits the squirrel.[(triple8 OR ((triple2) -> rule6) OR ((((triple3) -> rule4)) -> rule6) OR ((((((triple5) -> rule3)) -> rule4)) -> rule6))] The squirrel is big.[(triple9)] The squirrel is cold.[(triple10 OR ((triple11) -> rule4) OR ((((triple13) -> rule3)) -> rule4))] The squirrel is green.[(triple11 OR ((triple13) -> rule3))] The squirrel is red.[(triple12)] The squirrel is young.[(triple13)] The squirrel needs the dog.[(triple14)] The squirrel sees the dog.[(triple15)] The squirrel visits the dog.[(triple16 OR ((triple15 triple14) -> rule2))] @1: The squirrel needs the squirrel.[(((triple9 triple12) -> rule1))] The squirrel visits the squirrel.[(((triple10) -> rule6) OR ((((triple11) -> rule4)) -> rule6) OR ((((((triple13) -> rule3)) -> rule4)) -> rule6))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
((triple3) -> (rule4 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog is green.
("dog" "is" "green" "+")
triple3
((triple5) -> (rule3 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is red.
("dog" "is" "red" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple6
((triple1 triple4) -> (rule1 % int1))
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple7
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple8
((triple2) -> (rule6 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog is green.
("dog" "is" "green" "+")
int3
The squirrel is big.
("squirrel" "is" "big" "+")
triple9
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple10
((triple11) -> (rule4 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
((((triple13) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
triple11
((triple13) -> (rule3 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
triple12
The squirrel is young.
("squirrel" "is" "young" "+")
triple13
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple14
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple15
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple16
((triple15 triple14) -> (rule2 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((triple9 triple12) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple10) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
((((triple11) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((((triple13) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3