The cat is cold. The cat sees the cow. The cow is cold. The cow is kind. The cow is nice. The cow is red. The cow likes the mouse. The cow likes the squirrel. The mouse is young. The mouse needs the cat. The mouse needs the cow. The mouse sees the squirrel. The squirrel likes the cat. The squirrel needs the mouse. The squirrel sees the cat. If someone is cold and they like the mouse then the mouse likes the cat. If someone needs the mouse then they are cold. If someone likes the mouse then the mouse likes the cow. If someone is red and they see the cow then they need the cat. If someone likes the cow then they need the mouse. If the mouse likes the cow and the cow sees the mouse then the mouse is nice.
The cat is cold.
("cat" "is" "cold" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If someone is cold and they like the mouse then the mouse likes the cat.
((("someone" "is" "cold" "+") ("someone" "likes" "mouse" "+")) -> ("mouse" "likes" "cat" "+"))
If someone needs the mouse then they are cold.
((("someone" "needs" "mouse" "+")) -> ("someone" "is" "cold" "+"))
If someone likes the mouse then the mouse likes the cow.
((("someone" "likes" "mouse" "+")) -> ("mouse" "likes" "cow" "+"))
If someone is red and they see the cow then they need the cat.
((("someone" "is" "red" "+") ("someone" "sees" "cow" "+")) -> ("someone" "needs" "cat" "+"))
If someone likes the cow then they need the mouse.
((("someone" "likes" "cow" "+")) -> ("someone" "needs" "mouse" "+"))
If the mouse likes the cow and the cow sees the mouse then the mouse is nice.
((("mouse" "likes" "cow" "+") ("cow" "sees" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
The mouse needs the cat.
True
1
proof
[(triple10)]
("mouse" "needs" "cat" "+")
triple10
The mouse does not need the cat.
False
1
inv-proof
[(triple10)]
("mouse" "needs" "cat" "-")
triple10
The mouse likes the cat.
True
3
proof
[(((triple3 triple7) -> rule1))]
("mouse" "likes" "cat" "+")
((triple3 triple7) -> (rule1 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The squirrel is not cold.
False
2
inv-proof
[(((triple14) -> rule2))]
("squirrel" "is" "cold" "-")
((triple14) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The mouse needs the mouse.
True
3
proof
[(((((triple7) -> rule3)) -> rule5))]
("mouse" "needs" "mouse" "+")
((((triple7) -> (rule3 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse does not need the mouse.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule5))]
("mouse" "needs" "mouse" "-")
((((triple7) -> (rule3 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse is cold.
True
4
proof
[(((((((triple7) -> rule3)) -> rule5)) -> rule2))]
("mouse" "is" "cold" "+")
((((((triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int3
The mouse is not cold.
False
4
inv-proof
[(((((((triple7) -> rule3)) -> rule5)) -> rule2))]
("mouse" "is" "cold" "-")
((((((triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int3
The squirrel does not need the cat.
Unknown
inv-rconc
[@1: The squirrel needs the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "needs" "cat" "-")
The cow needs the mouse.
Unknown
rconc
[@1: The cow needs the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "needs" "mouse" "+")
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "needs" "cat" "-")
The cat needs the mouse.
Unknown
rconc
[@1: The cat needs the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "needs" "mouse" "+")
The squirrel is not kind.
Unknown
inv-random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "-")
The cat likes the cow.
Unknown
random
[@0: The cat likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cow" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The cat likes the squirrel.
Unknown
random
[@0: The cat likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "squirrel" "+")
@0: The cat is cold.[(triple1)] The cat sees the cow.[(triple2)] The cow is cold.[(triple3)] The cow is kind.[(triple4)] The cow is nice.[(triple5)] The cow is red.[(triple6)] The cow likes the mouse.[(triple7)] The cow likes the squirrel.[(triple8)] The mouse is young.[(triple9)] The mouse needs the cat.[(triple10)] The mouse needs the cow.[(triple11)] The mouse sees the squirrel.[(triple12)] The squirrel likes the cat.[(triple13)] The squirrel needs the mouse.[(triple14)] The squirrel sees the cat.[(triple15)] @1: The mouse likes the cat.[(((triple3 triple7) -> rule1))] The mouse likes the cow.[(((triple7) -> rule3))] The squirrel is cold.[(((triple14) -> rule2))] @2: The mouse needs the mouse.[(((((triple7) -> rule3)) -> rule5))] @3: The mouse is cold.[(((((((triple7) -> rule3)) -> rule5)) -> rule2))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat sees the cow.
("cat" "sees" "cow" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple3
The cow is kind.
("cow" "is" "kind" "+")
triple4
The cow is nice.
("cow" "is" "nice" "+")
triple5
The cow is red.
("cow" "is" "red" "+")
triple6
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple7
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple8
The mouse is young.
("mouse" "is" "young" "+")
triple9
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple10
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple11
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple12
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple13
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple14
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple15
The mouse likes the cat.
("mouse" "likes" "cat" "+")
((triple3 triple7) -> (rule1 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
((triple7) -> (rule3 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple14) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((triple7) -> (rule3 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
((((((triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int3