The cat eats the rabbit. The cat eats the squirrel. The cat likes the lion. The lion likes the cat. The lion visits the squirrel. The rabbit eats the lion. The rabbit eats the squirrel. The squirrel eats the rabbit. The squirrel is cold. The squirrel likes the cat. If someone eats the cat then they like the rabbit. If the lion likes the cat then the lion eats the cat. If someone visits the cat then they like the lion. If someone is round and red then they like the squirrel. If someone is cold and round then they visit the lion. If someone likes the squirrel then the squirrel eats the lion. If someone is cold then they visit the cat. If someone is cold and they like the lion then the lion is cold.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
If someone eats the cat then they like the rabbit.
((("someone" "eats" "cat" "+")) -> ("someone" "likes" "rabbit" "+"))
If the lion likes the cat then the lion eats the cat.
((("lion" "likes" "cat" "+")) -> ("lion" "eats" "cat" "+"))
If someone visits the cat then they like the lion.
((("someone" "visits" "cat" "+")) -> ("someone" "likes" "lion" "+"))
If someone is round and red then they like the squirrel.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone is cold and round then they visit the lion.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "visits" "lion" "+"))
If someone likes the squirrel then the squirrel eats the lion.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "eats" "lion" "+"))
If someone is cold then they visit the cat.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "cat" "+"))
If someone is cold and they like the lion then the lion is cold.
((("someone" "is" "cold" "+") ("someone" "likes" "lion" "+")) -> ("lion" "is" "cold" "+"))
The lion likes the cat.
True
1
proof
[(triple4)]
("lion" "likes" "cat" "+")
triple4
The cat does not eat the rabbit.
False
1
inv-proof
[(triple1)]
("cat" "eats" "rabbit" "-")
triple1
The squirrel visits the cat.
True
2
proof
[(((triple9) -> rule7))]
("squirrel" "visits" "cat" "+")
((triple9) -> (rule7 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel does not visit the cat.
False
2
inv-proof
[(((triple9) -> rule7))]
("squirrel" "visits" "cat" "-")
((triple9) -> (rule7 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The lion likes the rabbit.
True
3
proof
[(((((triple4) -> rule2)) -> rule1))]
("lion" "likes" "rabbit" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The squirrel does not like the lion.
False
3
inv-proof
[(((((triple9) -> rule7)) -> rule3))]
("squirrel" "likes" "lion" "-")
((((triple9) -> (rule7 % int2))) -> (rule3 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The lion is cold.
True
5
proof
[(((triple9 ((((triple9) -> rule7)) -> rule3)) -> rule8))]
("lion" "is" "cold" "+")
((triple9 ((((triple9) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int2
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int3
The lion is not cold.
False
5
inv-proof
[(((triple9 ((((triple9) -> rule7)) -> rule3)) -> rule8))]
("lion" "is" "cold" "-")
((triple9 ((((triple9) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int2
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int3
The lion visits the cat.
True
6
proof
[(((((triple9 ((((triple9) -> rule7)) -> rule3)) -> rule8)) -> rule7))]
("lion" "visits" "cat" "+")
((((triple9 ((((triple9) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int3
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int4
The lion does not visit the cat.
False
6
inv-proof
[(((((triple9 ((((triple9) -> rule7)) -> rule3)) -> rule8)) -> rule7))]
("lion" "visits" "cat" "-")
((((triple9 ((((triple9) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int3
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int4
The lion likes the lion.
True
7
proof
[(((((((triple9 ((((triple9) -> rule7)) -> rule3)) -> rule8)) -> rule7)) -> rule3))]
("lion" "likes" "lion" "+")
((((((triple9 ((((triple9) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int4
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int5
The lion does not like the lion.
False
7
inv-proof
[(((((((triple9 ((((triple9) -> rule7)) -> rule3)) -> rule8)) -> rule7)) -> rule3))]
("lion" "likes" "lion" "-")
((((((triple9 ((((triple9) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int4
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int5
The rabbit does not like the rabbit.
Unknown
inv-rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "likes" "rabbit" "-")
The rabbit visits the cat.
Unknown
rconc
[@1: The rabbit visits the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "visits" "cat" "+")
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The cat likes the rabbit.
Unknown
rconc
[@1: The cat likes the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "rabbit" "+")
The cat does not like the squirrel.
Unknown
inv-rconc
[@1: The cat likes the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "likes" "squirrel" "-")
The lion likes the squirrel.
Unknown
rconc
[@1: The lion likes the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "likes" "squirrel" "+")
The cat does not eat the lion.
Unknown
inv-random
[@0: The cat eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "lion" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The squirrel visits the rabbit.
Unknown
random
[@0: The squirrel visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "rabbit" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The cat eats the rabbit.[(triple1)] The cat eats the squirrel.[(triple2)] The cat likes the lion.[(triple3)] The lion likes the cat.[(triple4)] The lion visits the squirrel.[(triple5)] The rabbit eats the lion.[(triple6)] The rabbit eats the squirrel.[(triple7)] The squirrel eats the rabbit.[(triple8)] The squirrel is cold.[(triple9)] The squirrel likes the cat.[(triple10)] @1: The lion eats the cat.[(((triple4) -> rule2))] The squirrel visits the cat.[(((triple9) -> rule7))] @2: The lion likes the rabbit.[(((((triple4) -> rule2)) -> rule1))] The squirrel likes the lion.[(((((triple9) -> rule7)) -> rule3))] @3: The lion is cold.[(((triple9 ((((triple9) -> rule7)) -> rule3)) -> rule8))] @4: The lion visits the cat.[(((((triple9 ((((triple9) -> rule7)) -> rule3)) -> rule8)) -> rule7))] @5: The lion likes the lion.[(((((((triple9 ((((triple9) -> rule7)) -> rule3)) -> rule8)) -> rule7)) -> rule3))]
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple2
The cat likes the lion.
("cat" "likes" "lion" "+")
triple3
The lion likes the cat.
("lion" "likes" "cat" "+")
triple4
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple5
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple6
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple7
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple8
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple10
The lion eats the cat.
("lion" "eats" "cat" "+")
((triple4) -> (rule2 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((triple9) -> (rule7 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
((((triple9) -> (rule7 % int2))) -> (rule3 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
((triple9 ((((triple9) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int2
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int3
The lion visits the cat.
("lion" "visits" "cat" "+")
((((triple9 ((((triple9) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int3
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int4
The lion likes the lion.
("lion" "likes" "lion" "+")
((((((triple9 ((((triple9) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int4
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int5