The cat needs the lion. The lion is blue. The lion is round. The squirrel eats the lion. The squirrel eats the tiger. The tiger is rough. The tiger is round. If the cat visits the tiger and the cat is round then the cat is rough. If something eats the squirrel and it eats the cat then the squirrel eats the cat. If something is red then it visits the squirrel. If the cat eats the lion and the cat is round then the cat needs the squirrel. If something visits the squirrel and it visits the tiger then the squirrel eats the lion. If something is round then it is red. If something is green then it eats the tiger. If something needs the tiger and the tiger eats the cat then it eats the lion. If something visits the squirrel then the squirrel is round.
The cat needs the lion.
("cat" "needs" "lion" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is round.
("lion" "is" "round" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
If the cat visits the tiger and the cat is round then the cat is rough.
((("cat" "visits" "tiger" "+") ("cat" "is" "round" "+")) -> ("cat" "is" "rough" "+"))
If something eats the squirrel and it eats the cat then the squirrel eats the cat.
((("something" "eats" "squirrel" "+") ("something" "eats" "cat" "+")) -> ("squirrel" "eats" "cat" "+"))
If something is red then it visits the squirrel.
((("something" "is" "red" "+")) -> ("something" "visits" "squirrel" "+"))
If the cat eats the lion and the cat is round then the cat needs the squirrel.
((("cat" "eats" "lion" "+") ("cat" "is" "round" "+")) -> ("cat" "needs" "squirrel" "+"))
If something visits the squirrel and it visits the tiger then the squirrel eats the lion.
((("something" "visits" "squirrel" "+") ("something" "visits" "tiger" "+")) -> ("squirrel" "eats" "lion" "+"))
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is green then it eats the tiger.
((("something" "is" "green" "+")) -> ("something" "eats" "tiger" "+"))
If something needs the tiger and the tiger eats the cat then it eats the lion.
((("something" "needs" "tiger" "+") ("tiger" "eats" "cat" "+")) -> ("something" "eats" "lion" "+"))
If something visits the squirrel then the squirrel is round.
((("something" "visits" "squirrel" "+")) -> ("squirrel" "is" "round" "+"))
The lion is round.
True
1
proof
[(triple3)]
("lion" "is" "round" "+")
triple3
The lion is not round.
False
1
inv-proof
[(triple3)]
("lion" "is" "round" "-")
triple3
The lion is red.
True
2
proof
[(((triple3) -> rule6))]
("lion" "is" "red" "+")
((triple3) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The tiger is not red.
False
2
inv-proof
[(((triple7) -> rule6))]
("tiger" "is" "red" "-")
((triple7) -> (rule6 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger visits the squirrel.
True
3
proof
[(((((triple7) -> rule6)) -> rule3))]
("tiger" "visits" "squirrel" "+")
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger does not visit the squirrel.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule3))]
("tiger" "visits" "squirrel" "-")
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The squirrel is round.
True
4
proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule9) OR ((((((triple7) -> rule6)) -> rule3)) -> rule9))]
("squirrel" "is" "round" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
((((((triple7) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The squirrel is not round.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule9) OR ((((((triple7) -> rule6)) -> rule3)) -> rule9))]
("squirrel" "is" "round" "-")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
((((((triple7) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The squirrel is red.
True
5
proof
[(((((((((triple3) -> rule6)) -> rule3)) -> rule9)) -> rule6) OR ((((((((triple7) -> rule6)) -> rule3)) -> rule9)) -> rule6))]
("squirrel" "is" "red" "+")
((((((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
((((((((triple7) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
int4
The squirrel is not red.
False
5
inv-proof
[(((((((((triple3) -> rule6)) -> rule3)) -> rule9)) -> rule6) OR ((((((((triple7) -> rule6)) -> rule3)) -> rule9)) -> rule6))]
("squirrel" "is" "red" "-")
((((((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
((((((((triple7) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
int4
The squirrel visits the squirrel.
True
6
proof
[(((((((((((triple3) -> rule6)) -> rule3)) -> rule9)) -> rule6)) -> rule3) OR ((((((((((triple7) -> rule6)) -> rule3)) -> rule9)) -> rule6)) -> rule3))]
("squirrel" "visits" "squirrel" "+")
((((((((((triple3) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
((((((((((triple7) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int4
The tiger is red.
("tiger" "is" "red" "+")
int5
The squirrel does not visit the squirrel.
False
6
inv-proof
[(((((((((((triple3) -> rule6)) -> rule3)) -> rule9)) -> rule6)) -> rule3) OR ((((((((((triple7) -> rule6)) -> rule3)) -> rule9)) -> rule6)) -> rule3))]
("squirrel" "visits" "squirrel" "-")
((((((((((triple3) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
((((((((((triple7) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int4
The tiger is red.
("tiger" "is" "red" "+")
int5
The squirrel does not eat the cat.
Unknown
inv-rconc
[@1: The squirrel eats the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "eats" "cat" "-")
The cat is red.
Unknown
rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "red" "+")
The lion does not eat the tiger.
Unknown
inv-rconc
[@1: The lion eats the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "eats" "tiger" "-")
The cat eats the lion.
Unknown
rconc
[@1: The cat eats the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "eats" "lion" "+")
The cat does not visit the squirrel.
Unknown
inv-rconc
[@2: The cat visits the squirrel.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("cat" "visits" "squirrel" "-")
The tiger eats the tiger.
Unknown
rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "eats" "tiger" "+")
The lion does not need the tiger.
Unknown
inv-random
[@0: The lion needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "tiger" "-")
The squirrel visits the lion.
Unknown
random
[@0: The squirrel visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "lion" "+")
The tiger does not visit the lion.
Unknown
inv-random
[@0: The tiger visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "lion" "-")
The squirrel visits the cat.
Unknown
random
[@0: The squirrel visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "cat" "+")
The lion does not visit the cat.
Unknown
inv-random
[@0: The lion visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cat" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
@0: The cat needs the lion.[(triple1)] The lion is blue.[(triple2)] The lion is round.[(triple3)] The squirrel eats the lion.[(triple4)] The squirrel eats the tiger.[(triple5)] The tiger is rough.[(triple6)] The tiger is round.[(triple7)] @1: The lion is red.[(((triple3) -> rule6))] The tiger is red.[(((triple7) -> rule6))] @2: The lion visits the squirrel.[(((((triple3) -> rule6)) -> rule3))] The tiger visits the squirrel.[(((((triple7) -> rule6)) -> rule3))] @3: The squirrel is round.[(((((((triple3) -> rule6)) -> rule3)) -> rule9) OR ((((((triple7) -> rule6)) -> rule3)) -> rule9))] @4: The squirrel is red.[(((((((((triple3) -> rule6)) -> rule3)) -> rule9)) -> rule6) OR ((((((((triple7) -> rule6)) -> rule3)) -> rule9)) -> rule6))] @5: The squirrel visits the squirrel.[(((((((((((triple3) -> rule6)) -> rule3)) -> rule9)) -> rule6)) -> rule3) OR ((((((((((triple7) -> rule6)) -> rule3)) -> rule9)) -> rule6)) -> rule3))]
The cat needs the lion.
("cat" "needs" "lion" "+")
triple1
The lion is blue.
("lion" "is" "blue" "+")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple4
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple5
The tiger is rough.
("tiger" "is" "rough" "+")
triple6
The tiger is round.
("tiger" "is" "round" "+")
triple7
The lion is red.
("lion" "is" "red" "+")
((triple3) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
((triple7) -> (rule6 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
((((((triple7) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The squirrel is red.
("squirrel" "is" "red" "+")
((((((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
((((((((triple7) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
int4
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((((((((((triple3) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
((((((((((triple7) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int4
The tiger is red.
("tiger" "is" "red" "+")
int5