The cat is nice. The lion is cold. The squirrel eats the lion. If something eats the cat then it needs the lion. If something eats the squirrel and the squirrel needs the cat then it likes the squirrel. If something is cold and it needs the squirrel then it is big. If something eats the squirrel then it is round. If something is nice then it needs the cat. If something eats the squirrel and the squirrel eats the lion then the lion is nice. If something needs the cat then it eats the squirrel. If the cat likes the lion then the lion likes the squirrel.
The cat is nice.
("cat" "is" "nice" "+")
The lion is cold.
("lion" "is" "cold" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
If something eats the cat then it needs the lion.
((("something" "eats" "cat" "+")) -> ("something" "needs" "lion" "+"))
If something eats the squirrel and the squirrel needs the cat then it likes the squirrel.
((("something" "eats" "squirrel" "+") ("squirrel" "needs" "cat" "+")) -> ("something" "likes" "squirrel" "+"))
If something is cold and it needs the squirrel then it is big.
((("something" "is" "cold" "+") ("something" "needs" "squirrel" "+")) -> ("something" "is" "big" "+"))
If something eats the squirrel then it is round.
((("something" "eats" "squirrel" "+")) -> ("something" "is" "round" "+"))
If something is nice then it needs the cat.
((("something" "is" "nice" "+")) -> ("something" "needs" "cat" "+"))
If something eats the squirrel and the squirrel eats the lion then the lion is nice.
((("something" "eats" "squirrel" "+") ("squirrel" "eats" "lion" "+")) -> ("lion" "is" "nice" "+"))
If something needs the cat then it eats the squirrel.
((("something" "needs" "cat" "+")) -> ("something" "eats" "squirrel" "+"))
If the cat likes the lion then the lion likes the squirrel.
((("cat" "likes" "lion" "+")) -> ("lion" "likes" "squirrel" "+"))
The squirrel eats the lion.
True
1
proof
[(triple3)]
("squirrel" "eats" "lion" "+")
triple3
The lion is not cold.
False
1
inv-proof
[(triple2)]
("lion" "is" "cold" "-")
triple2
The cat needs the cat.
True
2
proof
[(((triple1) -> rule5))]
("cat" "needs" "cat" "+")
((triple1) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not need the cat.
False
2
inv-proof
[(((triple1) -> rule5))]
("cat" "needs" "cat" "-")
((triple1) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat eats the squirrel.
True
3
proof
[(((((triple1) -> rule5)) -> rule7))]
("cat" "eats" "squirrel" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat does not eat the squirrel.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule7))]
("cat" "eats" "squirrel" "-")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat is round.
True
4
proof
[(((((((triple1) -> rule5)) -> rule7)) -> rule4))]
("cat" "is" "round" "+")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The cat is not round.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule7)) -> rule4))]
("cat" "is" "round" "-")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The lion does not like the squirrel.
Unknown
inv-rconc
[@2: The lion likes the squirrel.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("lion" "likes" "squirrel" "-")
The squirrel needs the lion.
Unknown
rconc
[@1: The squirrel needs the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "needs" "lion" "+")
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@2: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The cat is big.
Unknown
rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "big" "+")
The squirrel does not like the lion.
Unknown
inv-random
[@0: The squirrel likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "lion" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The cat needs the squirrel.
Unknown
random
[@0: The cat needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "squirrel" "+")
@0: The cat is nice.[(triple1)] The lion is cold.[(triple2)] The squirrel eats the lion.[(triple3)] @1: The cat needs the cat.[(((triple1) -> rule5))] @2: The cat eats the squirrel.[(((((triple1) -> rule5)) -> rule7))] @3: The cat is round.[(((((((triple1) -> rule5)) -> rule7)) -> rule4))] The lion is nice.[(((((((triple1) -> rule5)) -> rule7) triple3) -> rule6))] @4: The lion needs the cat.[(((((((((triple1) -> rule5)) -> rule7) triple3) -> rule6)) -> rule5))] @5: The lion eats the squirrel.[(((((((((((triple1) -> rule5)) -> rule7) triple3) -> rule6)) -> rule5)) -> rule7))] @6: The lion is round.[(((((((((((((triple1) -> rule5)) -> rule7) triple3) -> rule6)) -> rule5)) -> rule7)) -> rule4))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple3
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple1) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The lion is nice.
("lion" "is" "nice" "+")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2)) triple3) -> (rule6 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The lion needs the cat.
("lion" "needs" "cat" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule7 % int3)) triple3) -> (rule6 % int2))) -> (rule5 % int1))
The lion needs the cat.
("lion" "needs" "cat" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int3
The cat needs the cat.
("cat" "needs" "cat" "+")
int4
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
((((((((((triple1) -> (rule5 % int5))) -> (rule7 % int4)) triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int4
The cat needs the cat.
("cat" "needs" "cat" "+")
int5
The lion is round.
("lion" "is" "round" "+")
((((((((((((triple1) -> (rule5 % int6))) -> (rule7 % int5)) triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
The lion needs the cat.
("lion" "needs" "cat" "+")
int3
The lion is nice.
("lion" "is" "nice" "+")
int4
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int5
The cat needs the cat.
("cat" "needs" "cat" "+")
int6