The dog is big. The dog is blue. The dog is cold. The dog is not rough. The dog is young. The dog needs the squirrel. The dog does not see the squirrel. The dog visits the squirrel. The squirrel is big. The squirrel is blue. The squirrel is not cold. The squirrel is rough. The squirrel is young. The squirrel needs the dog. The squirrel sees the dog. The squirrel does not visit the dog. If someone is cold then they need the dog. If someone needs the dog and they need the squirrel then they visit the dog.
The dog is big.
("dog" "is" "big" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is not rough.
("dog" "is" "rough" "-")
The dog is young.
("dog" "is" "young" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The dog does not see the squirrel.
("dog" "sees" "squirrel" "-")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is not cold.
("squirrel" "is" "cold" "-")
The squirrel is rough.
("squirrel" "is" "rough" "+")
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 does not visit the dog.
("squirrel" "visits" "dog" "-")
If someone is cold then they need the dog.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "dog" "+"))
If someone needs the dog and they need the squirrel then they visit the dog.
((("someone" "needs" "dog" "+") ("someone" "needs" "squirrel" "+")) -> ("someone" "visits" "dog" "+"))
The squirrel does not visit the dog.
True
1
proof
[(triple16)]
("squirrel" "visits" "dog" "-")
triple16
The squirrel does not see the dog.
False
1
inv-proof
[(triple15)]
("squirrel" "sees" "dog" "-")
triple15
The dog needs the dog.
True
2
proof
[(((triple3) -> rule1))]
("dog" "needs" "dog" "+")
((triple3) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog does not need the dog.
False
2
inv-proof
[(((triple3) -> rule1))]
("dog" "needs" "dog" "-")
((triple3) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the dog.
True
4
proof
[(((((triple3) -> rule1) triple6) -> rule2))]
("dog" "visits" "dog" "+")
((((triple3) -> (rule1 % int2)) triple6) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog does not visit the dog.
False
4
inv-proof
[(((((triple3) -> rule1) triple6) -> rule2))]
("dog" "visits" "dog" "-")
((((triple3) -> (rule1 % int2)) triple6) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
@0: The dog does not see the squirrel.[(triple7)] The dog is big.[(triple1)] The dog is blue.[(triple2)] The dog is cold.[(triple3)] The dog is not rough.[(triple4)] The dog is young.[(triple5)] The dog needs the squirrel.[(triple6)] The dog visits the squirrel.[(triple8)] The squirrel does not visit the dog.[(triple16)] The squirrel is big.[(triple9)] The squirrel is blue.[(triple10)] The squirrel is not cold.[(triple11)] The squirrel is rough.[(triple12)] The squirrel is young.[(triple13)] The squirrel needs the dog.[(triple14)] The squirrel sees the dog.[(triple15)] @1: The dog needs the dog.[(((triple3) -> rule1))] @2: The dog visits the dog.[(((((triple3) -> rule1) triple6) -> rule2))]
The dog does not see the squirrel.
("dog" "sees" "squirrel" "-")
triple7
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is not rough.
("dog" "is" "rough" "-")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple6
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple8
The squirrel does not visit the dog.
("squirrel" "visits" "dog" "-")
triple16
The squirrel is big.
("squirrel" "is" "big" "+")
triple9
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple10
The squirrel is not cold.
("squirrel" "is" "cold" "-")
triple11
The squirrel is rough.
("squirrel" "is" "rough" "+")
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 dog needs the dog.
("dog" "needs" "dog" "+")
((triple3) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((((triple3) -> (rule1 % int2)) triple6) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2