The cat is big. The cat is kind. The cat is rough. The cat needs the dog. The cat needs the squirrel. The dog eats the cat. The dog needs the cat. The dog needs the squirrel. The mouse is blue. The mouse is cold. The mouse is kind. The mouse needs the squirrel. The mouse sees the squirrel. The squirrel is cold. The squirrel needs the dog. The squirrel needs the mouse. If something needs the mouse then it sees the cat. If something is cold and it sees the cat then it eats the dog.
The cat is big.
("cat" "is" "big" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If something needs the mouse then it sees the cat.
((("something" "needs" "mouse" "+")) -> ("something" "sees" "cat" "+"))
If something is cold and it sees the cat then it eats the dog.
((("something" "is" "cold" "+") ("something" "sees" "cat" "+")) -> ("something" "eats" "dog" "+"))
The cat needs the dog.
True
1
proof
[(triple4)]
("cat" "needs" "dog" "+")
triple4
The squirrel does not need the mouse.
False
1
inv-proof
[(triple16)]
("squirrel" "needs" "mouse" "-")
triple16
The squirrel sees the cat.
True
2
proof
[(((triple16) -> rule1))]
("squirrel" "sees" "cat" "+")
((triple16) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The squirrel does not see the cat.
False
2
inv-proof
[(((triple16) -> rule1))]
("squirrel" "sees" "cat" "-")
((triple16) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The squirrel eats the dog.
True
4
proof
[(((triple14 ((triple16) -> rule1)) -> rule2))]
("squirrel" "eats" "dog" "+")
((triple14 ((triple16) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The squirrel does not eat the dog.
False
4
inv-proof
[(((triple14 ((triple16) -> rule1)) -> rule2))]
("squirrel" "eats" "dog" "-")
((triple14 ((triple16) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "cat" "-")
The cat eats the dog.
Unknown
rconc
[@1: The cat eats the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "eats" "dog" "+")
The mouse does not see the cat.
Unknown
inv-rconc
[@1: The mouse sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "cat" "-")
The squirrel sees the dog.
Unknown
random
[@0: The squirrel sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "dog" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat is big.[(triple1)] The cat is kind.[(triple2)] The cat is rough.[(triple3)] The cat needs the dog.[(triple4)] The cat needs the squirrel.[(triple5)] The dog eats the cat.[(triple6)] The dog needs the cat.[(triple7)] The dog needs the squirrel.[(triple8)] The mouse is blue.[(triple9)] The mouse is cold.[(triple10)] The mouse is kind.[(triple11)] The mouse needs the squirrel.[(triple12)] The mouse sees the squirrel.[(triple13)] The squirrel is cold.[(triple14)] The squirrel needs the dog.[(triple15)] The squirrel needs the mouse.[(triple16)] @1: The squirrel sees the cat.[(((triple16) -> rule1))] @2: The squirrel eats the dog.[(((triple14 ((triple16) -> rule1)) -> rule2))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat needs the dog.
("cat" "needs" "dog" "+")
triple4
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple5
The dog eats the cat.
("dog" "eats" "cat" "+")
triple6
The dog needs the cat.
("dog" "needs" "cat" "+")
triple7
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple8
The mouse is blue.
("mouse" "is" "blue" "+")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
The mouse is kind.
("mouse" "is" "kind" "+")
triple11
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple12
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple13
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple14
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple15
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple16
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
((triple16) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
((triple14 ((triple16) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2