The cat is not cold. The cat needs the squirrel. The dog eats the squirrel. The mouse does not eat the cat. The mouse is young. The squirrel does not eat the dog. The squirrel is cold. If the cat is red and the cat is rough then the cat does not chase the dog. If someone eats the mouse then they need the mouse. If the dog eats the squirrel then the dog eats the mouse. If someone needs the squirrel then they do not need the cat. If someone is rough and they eat the squirrel then the squirrel needs the mouse. If someone eats the squirrel and they need the mouse then the mouse needs the cat.
The cat is not cold.
("cat" "is" "cold" "-")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The mouse does not eat the cat.
("mouse" "eats" "cat" "-")
The mouse is young.
("mouse" "is" "young" "+")
The squirrel does not eat the dog.
("squirrel" "eats" "dog" "-")
The squirrel is cold.
("squirrel" "is" "cold" "+")
If the cat is red and the cat is rough then the cat does not chase the dog.
((("cat" "is" "red" "+") ("cat" "is" "rough" "+")) -> ("cat" "chases" "dog" "-"))
If someone eats the mouse then they need the mouse.
((("someone" "eats" "mouse" "+")) -> ("someone" "needs" "mouse" "+"))
If the dog eats the squirrel then the dog eats the mouse.
((("dog" "eats" "squirrel" "+")) -> ("dog" "eats" "mouse" "+"))
If someone needs the squirrel then they do not need the cat.
((("someone" "needs" "squirrel" "+")) -> ("someone" "needs" "cat" "-"))
If someone is rough and they eat the squirrel then the squirrel needs the mouse.
((("someone" "is" "rough" "+") ("someone" "eats" "squirrel" "+")) -> ("squirrel" "needs" "mouse" "+"))
If someone eats the squirrel and they need the mouse then the mouse needs the cat.
((("someone" "eats" "squirrel" "+") ("someone" "needs" "mouse" "+")) -> ("mouse" "needs" "cat" "+"))
The mouse is young.
True
1
proof
[(triple5)]
("mouse" "is" "young" "+")
triple5
The squirrel eats the dog.
False
1
inv-proof
[(triple6)]
("squirrel" "eats" "dog" "+")
triple6
The cat does not need the cat.
True
2
proof
[(((triple2) -> rule4))]
("cat" "needs" "cat" "-")
((triple2) -> (rule4 % int1))
The cat does not need the cat.
("cat" "needs" "cat" "-")
int1
The cat needs the cat.
False
2
inv-proof
[(((triple2) -> rule4))]
("cat" "needs" "cat" "+")
((triple2) -> (rule4 % int1))
The cat does not need the cat.
("cat" "needs" "cat" "-")
int1
The dog needs the mouse.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("dog" "needs" "mouse" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The dog does not need the mouse.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("dog" "needs" "mouse" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The mouse needs the cat.
True
5
proof
[(((triple3 ((((triple3) -> rule3)) -> rule2)) -> rule6))]
("mouse" "needs" "cat" "+")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int3
The mouse does not need the cat.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule3)) -> rule2)) -> rule6))]
("mouse" "needs" "cat" "-")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int3
The squirrel does not need the mouse.
Unknown
inv-rconc
[@1: The squirrel needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "needs" "mouse" "-")
The cat needs the mouse.
Unknown
rconc
[@1: The cat needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "needs" "mouse" "+")
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The dog eats the cat.
Unknown
random
[@0: The dog eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cat" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
The dog does not chase the squirrel.
Unknown
inv-random
[@0: The dog chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "squirrel" "-")
The mouse eats the squirrel.
Unknown
random
[@0: The mouse eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "squirrel" "+")
@0: The cat is not cold.[(triple1)] The cat needs the squirrel.[(triple2)] The dog eats the squirrel.[(triple3)] The mouse does not eat the cat.[(triple4)] The mouse is young.[(triple5)] The squirrel does not eat the dog.[(triple6)] The squirrel is cold.[(triple7)] @1: The cat does not need the cat.[(((triple2) -> rule4))] The dog eats the mouse.[(((triple3) -> rule3))] @2: The dog needs the mouse.[(((((triple3) -> rule3)) -> rule2))] @3: The mouse needs the cat.[(((triple3 ((((triple3) -> rule3)) -> rule2)) -> rule6))]
The cat is not cold.
("cat" "is" "cold" "-")
triple1
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple3
The mouse does not eat the cat.
("mouse" "eats" "cat" "-")
triple4
The mouse is young.
("mouse" "is" "young" "+")
triple5
The squirrel does not eat the dog.
("squirrel" "eats" "dog" "-")
triple6
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple7
The cat does not need the cat.
("cat" "needs" "cat" "-")
((triple2) -> (rule4 % int1))
The cat does not need the cat.
("cat" "needs" "cat" "-")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
((triple3) -> (rule3 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The mouse needs the cat.
("mouse" "needs" "cat" "+")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int3