The cat eats the lion. The cat is nice. The cat is rough. The cat sees the squirrel. The lion eats the squirrel. The lion is rough. The lion needs the squirrel. The rabbit needs the cat. The rabbit sees the cat. The rabbit sees the lion. The squirrel eats the rabbit. The squirrel is nice. The squirrel is rough. The squirrel needs the cat. The squirrel needs the lion. The squirrel needs the rabbit. If someone sees the rabbit then the rabbit is blue. If someone sees the rabbit then they are blue. If someone needs the lion then they eat the rabbit. If someone is blue then they need the lion. If someone eats the lion then they need the lion. If someone sees the squirrel then they eat the rabbit. If someone needs the cat and the cat needs the lion then the cat sees the rabbit. If someone is green and they need the rabbit then they are nice. If the lion needs the cat then the cat is green.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
If someone sees the rabbit then the rabbit is blue.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "is" "blue" "+"))
If someone sees the rabbit then they are blue.
((("someone" "sees" "rabbit" "+")) -> ("someone" "is" "blue" "+"))
If someone needs the lion then they eat the rabbit.
((("someone" "needs" "lion" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone is blue then they need the lion.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "lion" "+"))
If someone eats the lion then they need the lion.
((("someone" "eats" "lion" "+")) -> ("someone" "needs" "lion" "+"))
If someone sees the squirrel then they eat the rabbit.
((("someone" "sees" "squirrel" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone needs the cat and the cat needs the lion then the cat sees the rabbit.
((("someone" "needs" "cat" "+") ("cat" "needs" "lion" "+")) -> ("cat" "sees" "rabbit" "+"))
If someone is green and they need the rabbit then they are nice.
((("someone" "is" "green" "+") ("someone" "needs" "rabbit" "+")) -> ("someone" "is" "nice" "+"))
If the lion needs the cat then the cat is green.
((("lion" "needs" "cat" "+")) -> ("cat" "is" "green" "+"))
The lion is rough.
True
1
proof
[(triple6)]
("lion" "is" "rough" "+")
triple6
The squirrel does not need the lion.
False
1
inv-proof
[(triple15)]
("squirrel" "needs" "lion" "-")
triple15
The cat eats the rabbit.
True
2
proof
[(((triple4) -> rule6) OR ((((triple1) -> rule5)) -> rule3))]
("cat" "eats" "rabbit" "+")
((triple4) -> (rule6 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The cat does not need the lion.
False
2
inv-proof
[(((triple1) -> rule5))]
("cat" "needs" "lion" "-")
((triple1) -> (rule5 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The cat sees the rabbit.
True
4
proof
[(((triple14 ((triple1) -> rule5)) -> rule7) OR ((triple8 ((triple1) -> rule5)) -> rule7))]
("cat" "sees" "rabbit" "+")
((triple14 ((triple1) -> (rule5 % int2))) -> (rule7 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
((triple8 ((triple1) -> (rule5 % int2))) -> (rule7 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The cat does not see the rabbit.
False
4
inv-proof
[(((triple14 ((triple1) -> rule5)) -> rule7) OR ((triple8 ((triple1) -> rule5)) -> rule7))]
("cat" "sees" "rabbit" "-")
((triple14 ((triple1) -> (rule5 % int2))) -> (rule7 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
((triple8 ((triple1) -> (rule5 % int2))) -> (rule7 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The cat is blue.
True
5
proof
[(((((triple14 ((triple1) -> rule5)) -> rule7)) -> rule2) OR ((((triple8 ((triple1) -> rule5)) -> rule7)) -> rule2))]
("cat" "is" "blue" "+")
((((triple14 ((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
int3
((((triple8 ((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
int3
The rabbit is not blue.
False
5
inv-proof
[(((((triple14 ((triple1) -> rule5)) -> rule7)) -> rule1) OR ((((triple8 ((triple1) -> rule5)) -> rule7)) -> rule1))]
("rabbit" "is" "blue" "-")
((((triple14 ((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
int3
((((triple8 ((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
int3
The rabbit needs the lion.
True
6
proof
[(((((((triple14 ((triple1) -> rule5)) -> rule7)) -> rule1)) -> rule4) OR ((((((triple8 ((triple1) -> rule5)) -> rule7)) -> rule1)) -> rule4))]
("rabbit" "needs" "lion" "+")
((((((triple14 ((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int3
The cat needs the lion.
("cat" "needs" "lion" "+")
int4
((((((triple8 ((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int3
The cat needs the lion.
("cat" "needs" "lion" "+")
int4
The rabbit does not need the lion.
False
6
inv-proof
[(((((((triple14 ((triple1) -> rule5)) -> rule7)) -> rule1)) -> rule4) OR ((((((triple8 ((triple1) -> rule5)) -> rule7)) -> rule1)) -> rule4))]
("rabbit" "needs" "lion" "-")
((((((triple14 ((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int3
The cat needs the lion.
("cat" "needs" "lion" "+")
int4
((((((triple8 ((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int3
The cat needs the lion.
("cat" "needs" "lion" "+")
int4
The rabbit eats the rabbit.
True
7
proof
[(((((((((triple14 ((triple1) -> rule5)) -> rule7)) -> rule1)) -> rule4)) -> rule3) OR ((((((((triple8 ((triple1) -> rule5)) -> rule7)) -> rule1)) -> rule4)) -> rule3))]
("rabbit" "eats" "rabbit" "+")
((((((((triple14 ((triple1) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int4
The cat needs the lion.
("cat" "needs" "lion" "+")
int5
((((((((triple8 ((triple1) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int4
The cat needs the lion.
("cat" "needs" "lion" "+")
int5
The rabbit does not eat the rabbit.
False
7
inv-proof
[(((((((((triple14 ((triple1) -> rule5)) -> rule7)) -> rule1)) -> rule4)) -> rule3) OR ((((((((triple8 ((triple1) -> rule5)) -> rule7)) -> rule1)) -> rule4)) -> rule3))]
("rabbit" "eats" "rabbit" "-")
((((((((triple14 ((triple1) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int4
The cat needs the lion.
("cat" "needs" "lion" "+")
int5
((((((((triple8 ((triple1) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int4
The cat needs the lion.
("cat" "needs" "lion" "+")
int5
The lion is not blue.
Unknown
inv-rconc
[@1: The lion is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "blue" "-")
The lion needs the lion.
Unknown
rconc
[@2: The lion needs the lion.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("lion" "needs" "lion" "+")
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "is" "nice" "-")
The cat is green.
Unknown
rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("cat" "is" "green" "+")
The lion does not eat the rabbit.
Unknown
inv-rconc
[@3: The lion eats the rabbit.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule2 <- FAIL)]]
("lion" "eats" "rabbit" "-")
The squirrel is blue.
Unknown
rconc
[@1: The squirrel is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "blue" "+")
The lion does not need the rabbit.
Unknown
inv-random
[@0: The lion needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "rabbit" "-")
The squirrel eats the lion.
Unknown
random
[@0: The squirrel eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "lion" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The lion sees the cat.
Unknown
random
[@0: The lion sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cat" "+")
The lion does not see the squirrel.
Unknown
inv-random
[@0: The lion sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "squirrel" "-")
The lion sees the rabbit.
Unknown
random
[@0: The lion sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "rabbit" "+")
@0: The cat eats the lion.[(triple1)] The cat is nice.[(triple2)] The cat is rough.[(triple3)] The cat sees the squirrel.[(triple4)] The lion eats the squirrel.[(triple5)] The lion is rough.[(triple6)] The lion needs the squirrel.[(triple7)] The rabbit needs the cat.[(triple8)] The rabbit sees the cat.[(triple9)] The rabbit sees the lion.[(triple10)] The squirrel eats the rabbit.[(triple11 OR ((triple15) -> rule3))] The squirrel is nice.[(triple12)] The squirrel is rough.[(triple13)] The squirrel needs the cat.[(triple14)] The squirrel needs the lion.[(triple15)] The squirrel needs the rabbit.[(triple16)] @1: The cat eats the rabbit.[(((triple4) -> rule6) OR ((((triple1) -> rule5)) -> rule3))] The cat needs the lion.[(((triple1) -> rule5))] @2: The cat sees the rabbit.[(((triple14 ((triple1) -> rule5)) -> rule7) OR ((triple8 ((triple1) -> rule5)) -> rule7))] @3: The cat is blue.[(((((triple14 ((triple1) -> rule5)) -> rule7)) -> rule2) OR ((((triple8 ((triple1) -> rule5)) -> rule7)) -> rule2))] The rabbit is blue.[(((((triple14 ((triple1) -> rule5)) -> rule7)) -> rule1) OR ((((triple8 ((triple1) -> rule5)) -> rule7)) -> rule1))] @4: The rabbit needs the lion.[(((((((triple14 ((triple1) -> rule5)) -> rule7)) -> rule1)) -> rule4) OR ((((((triple8 ((triple1) -> rule5)) -> rule7)) -> rule1)) -> rule4))] @5: The rabbit eats the rabbit.[(((((((((triple14 ((triple1) -> rule5)) -> rule7)) -> rule1)) -> rule4)) -> rule3) OR ((((((((triple8 ((triple1) -> rule5)) -> rule7)) -> rule1)) -> rule4)) -> rule3))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple4
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple5
The lion is rough.
("lion" "is" "rough" "+")
triple6
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple7
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple8
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple9
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple10
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple11
((triple15) -> (rule3 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple12
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple13
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple14
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple15
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple16
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
((triple4) -> (rule6 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
((triple1) -> (rule5 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
((triple14 ((triple1) -> (rule5 % int2))) -> (rule7 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
((triple8 ((triple1) -> (rule5 % int2))) -> (rule7 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
((((triple14 ((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
int3
((((triple8 ((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
int3
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((triple14 ((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
int3
((((triple8 ((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
int3
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
((((((triple14 ((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int3
The cat needs the lion.
("cat" "needs" "lion" "+")
int4
((((((triple8 ((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int3
The cat needs the lion.
("cat" "needs" "lion" "+")
int4
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((((((triple14 ((triple1) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int4
The cat needs the lion.
("cat" "needs" "lion" "+")
int5
((((((((triple8 ((triple1) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int4
The cat needs the lion.
("cat" "needs" "lion" "+")
int5