The cat chases the squirrel. The cat likes the rabbit. The cat needs the squirrel. The mouse does not chase the squirrel. The rabbit is kind. The rabbit likes the mouse. The squirrel needs the rabbit. If something likes the squirrel and the squirrel needs the rabbit then the rabbit likes the squirrel. If something is cold then it needs the mouse. If something chases the squirrel then the squirrel likes the mouse. If something is green and kind then it is nice. If something likes the rabbit and the rabbit is rough then the rabbit is cold. If something likes the rabbit then the rabbit needs the cat. If something is kind then it is cold. If something needs the mouse then the mouse is kind. If something chases the squirrel and the squirrel likes the cat then it is not green.
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The mouse does not chase the squirrel.
("mouse" "chases" "squirrel" "-")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
If something likes the squirrel and the squirrel needs the rabbit then the rabbit likes the squirrel.
((("something" "likes" "squirrel" "+") ("squirrel" "needs" "rabbit" "+")) -> ("rabbit" "likes" "squirrel" "+"))
If something is cold then it needs the mouse.
((("something" "is" "cold" "+")) -> ("something" "needs" "mouse" "+"))
If something chases the squirrel then the squirrel likes the mouse.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "likes" "mouse" "+"))
If something is green and kind then it is nice.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something likes the rabbit and the rabbit is rough then the rabbit is cold.
((("something" "likes" "rabbit" "+") ("rabbit" "is" "rough" "+")) -> ("rabbit" "is" "cold" "+"))
If something likes the rabbit then the rabbit needs the cat.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "needs" "cat" "+"))
If something is kind then it is cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something needs the mouse then the mouse is kind.
((("something" "needs" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If something chases the squirrel and the squirrel likes the cat then it is not green.
((("something" "chases" "squirrel" "+") ("squirrel" "likes" "cat" "+")) -> ("something" "is" "green" "-"))
The cat chases the squirrel.
True
1
proof
[(triple1)]
("cat" "chases" "squirrel" "+")
triple1
The rabbit is not kind.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "kind" "-")
triple5
The squirrel likes the mouse.
True
2
proof
[(((triple1) -> rule3))]
("squirrel" "likes" "mouse" "+")
((triple1) -> (rule3 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The squirrel does not like the mouse.
False
2
inv-proof
[(((triple1) -> rule3))]
("squirrel" "likes" "mouse" "-")
((triple1) -> (rule3 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The rabbit needs the mouse.
True
3
proof
[(((((triple5) -> rule7)) -> rule2))]
("rabbit" "needs" "mouse" "+")
((((triple5) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit does not need the mouse.
False
3
inv-proof
[(((((triple5) -> rule7)) -> rule2))]
("rabbit" "needs" "mouse" "-")
((((triple5) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The mouse is kind.
True
4
proof
[(((((((triple5) -> rule7)) -> rule2)) -> rule8))]
("mouse" "is" "kind" "+")
((((((triple5) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The mouse is not kind.
False
4
inv-proof
[(((((((triple5) -> rule7)) -> rule2)) -> rule8))]
("mouse" "is" "kind" "-")
((((((triple5) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The mouse is cold.
True
5
proof
[(((((((((triple5) -> rule7)) -> rule2)) -> rule8)) -> rule7))]
("mouse" "is" "cold" "+")
((((((((triple5) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
int4
The mouse is not cold.
False
5
inv-proof
[(((((((((triple5) -> rule7)) -> rule2)) -> rule8)) -> rule7))]
("mouse" "is" "cold" "-")
((((((((triple5) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
int4
The mouse needs the mouse.
True
6
proof
[(((((((((((triple5) -> rule7)) -> rule2)) -> rule8)) -> rule7)) -> rule2))]
("mouse" "needs" "mouse" "+")
((((((((((triple5) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int4
The rabbit is cold.
("rabbit" "is" "cold" "+")
int5
The mouse does not need the mouse.
False
6
inv-proof
[(((((((((((triple5) -> rule7)) -> rule2)) -> rule8)) -> rule7)) -> rule2))]
("mouse" "needs" "mouse" "-")
((((((((((triple5) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int4
The rabbit is cold.
("rabbit" "is" "cold" "+")
int5
The squirrel does not need the mouse.
Unknown
inv-rconc
[@2: The squirrel needs the mouse.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("squirrel" "needs" "mouse" "-")
The rabbit likes the squirrel.
Unknown
rconc
[@1: The rabbit likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "likes" "squirrel" "+")
The cat is not cold.
Unknown
inv-rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "cold" "-")
The cat needs the mouse.
Unknown
rconc
[@2: The cat needs the mouse.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("cat" "needs" "mouse" "+")
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "nice" "-")
The squirrel is cold.
Unknown
rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "cold" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse likes the cat.
Unknown
random
[@0: The mouse likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "cat" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
The cat does not like the squirrel.
Unknown
inv-random
[@0: The cat likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "squirrel" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The cat chases the squirrel.[(triple1)] The cat likes the rabbit.[(triple2)] The cat needs the squirrel.[(triple3)] The mouse does not chase the squirrel.[(triple4)] The rabbit is kind.[(triple5)] The rabbit likes the mouse.[(triple6)] The squirrel needs the rabbit.[(triple7)] @1: The rabbit is cold.[(((triple5) -> rule7))] The rabbit needs the cat.[(((triple2) -> rule6))] The squirrel likes the mouse.[(((triple1) -> rule3))] @2: The rabbit needs the mouse.[(((((triple5) -> rule7)) -> rule2))] @3: The mouse is kind.[(((((((triple5) -> rule7)) -> rule2)) -> rule8))] @4: The mouse is cold.[(((((((((triple5) -> rule7)) -> rule2)) -> rule8)) -> rule7))] @5: The mouse needs the mouse.[(((((((((((triple5) -> rule7)) -> rule2)) -> rule8)) -> rule7)) -> rule2))]
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple2
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple3
The mouse does not chase the squirrel.
("mouse" "chases" "squirrel" "-")
triple4
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple5
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple6
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple5) -> (rule7 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
((triple2) -> (rule6 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
((triple1) -> (rule3 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
((((triple5) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
((((((triple5) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
((((((((triple5) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
int4
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((((((((triple5) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int4
The rabbit is cold.
("rabbit" "is" "cold" "+")
int5