The cow is kind. The cow visits the lion. The cow visits the squirrel. The lion needs the cow. The mouse eats the cow. The mouse eats the squirrel. The mouse is round. The mouse needs the squirrel. The mouse visits the cow. The squirrel eats the lion. The squirrel eats the mouse. The squirrel needs the cow. The squirrel visits the cow. The squirrel visits the lion. If something is red then it needs the mouse. If something eats the lion then it is red. If something eats the cow then it is round. If something eats the mouse and it needs the mouse then the mouse eats the lion. If the mouse eats the lion and the lion needs the cow then the cow needs the mouse.
The cow is kind.
("cow" "is" "kind" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something is red then it needs the mouse.
((("something" "is" "red" "+")) -> ("something" "needs" "mouse" "+"))
If something eats the lion then it is red.
((("something" "eats" "lion" "+")) -> ("something" "is" "red" "+"))
If something eats the cow then it is round.
((("something" "eats" "cow" "+")) -> ("something" "is" "round" "+"))
If something eats the mouse and it needs the mouse then the mouse eats the lion.
((("something" "eats" "mouse" "+") ("something" "needs" "mouse" "+")) -> ("mouse" "eats" "lion" "+"))
If the mouse eats the lion and the lion needs the cow then the cow needs the mouse.
((("mouse" "eats" "lion" "+") ("lion" "needs" "cow" "+")) -> ("cow" "needs" "mouse" "+"))
The squirrel needs the cow.
True
1
proof
[(triple12)]
("squirrel" "needs" "cow" "+")
triple12
The cow does not visit the squirrel.
False
1
inv-proof
[(triple3)]
("cow" "visits" "squirrel" "-")
triple3
The squirrel is red.
True
2
proof
[(((triple10) -> rule2))]
("squirrel" "is" "red" "+")
((triple10) -> (rule2 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is not red.
False
2
inv-proof
[(((triple10) -> rule2))]
("squirrel" "is" "red" "-")
((triple10) -> (rule2 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel needs the mouse.
True
3
proof
[(((((triple10) -> rule2)) -> rule1))]
("squirrel" "needs" "mouse" "+")
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel does not need the mouse.
False
3
inv-proof
[(((((triple10) -> rule2)) -> rule1))]
("squirrel" "needs" "mouse" "-")
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The mouse eats the lion.
True
5
proof
[(((triple11 ((((triple10) -> rule2)) -> rule1)) -> rule4))]
("mouse" "eats" "lion" "+")
((triple11 ((((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The mouse does not eat the lion.
False
5
inv-proof
[(((triple11 ((((triple10) -> rule2)) -> rule1)) -> rule4))]
("mouse" "eats" "lion" "-")
((triple11 ((((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The cow needs the mouse.
True
7
proof
[(((((triple11 ((((triple10) -> rule2)) -> rule1)) -> rule4) triple4) -> rule5))]
("cow" "needs" "mouse" "+")
((((triple11 ((((triple10) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple4) -> (rule5 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int3
The squirrel is red.
("squirrel" "is" "red" "+")
int4
The mouse is not red.
False
6
inv-proof
[(((((triple11 ((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule2))]
("mouse" "is" "red" "-")
((((triple11 ((((triple10) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int3
The squirrel is red.
("squirrel" "is" "red" "+")
int4
The mouse needs the mouse.
True
7
proof
[(((((((triple11 ((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule2)) -> rule1))]
("mouse" "needs" "mouse" "+")
((((((triple11 ((((triple10) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int4
The squirrel is red.
("squirrel" "is" "red" "+")
int5
The mouse does not need the mouse.
False
7
inv-proof
[(((((((triple11 ((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule2)) -> rule1))]
("mouse" "needs" "mouse" "-")
((((((triple11 ((((triple10) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int4
The squirrel is red.
("squirrel" "is" "red" "+")
int5
The cow is not red.
Unknown
inv-rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "red" "-")
The cow is round.
Unknown
rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "round" "+")
The squirrel is not round.
Unknown
inv-rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "round" "-")
The lion is round.
Unknown
rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "round" "+")
The lion does not need the mouse.
Unknown
inv-rconc
[@2: The lion needs the mouse.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("lion" "needs" "mouse" "-")
The lion is red.
Unknown
rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "red" "+")
The mouse does not need the cow.
Unknown
inv-random
[@0: The mouse needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cow" "-")
The lion eats the squirrel.
Unknown
random
[@0: The lion eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "squirrel" "+")
The cow does not need the squirrel.
Unknown
inv-random
[@0: The cow needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "squirrel" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
The cow does not eat the lion.
Unknown
inv-random
[@0: The cow eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "lion" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The cow is kind.[(triple1)] The cow visits the lion.[(triple2)] The cow visits the squirrel.[(triple3)] The lion needs the cow.[(triple4)] The mouse eats the cow.[(triple5)] The mouse eats the squirrel.[(triple6)] The mouse is round.[(triple7 OR ((triple5) -> rule3))] The mouse needs the squirrel.[(triple8)] The mouse visits the cow.[(triple9)] The squirrel eats the lion.[(triple10)] The squirrel eats the mouse.[(triple11)] The squirrel needs the cow.[(triple12)] The squirrel visits the cow.[(triple13)] The squirrel visits the lion.[(triple14)] @1: The squirrel is red.[(((triple10) -> rule2))] @2: The squirrel needs the mouse.[(((((triple10) -> rule2)) -> rule1))] @3: The mouse eats the lion.[(((triple11 ((((triple10) -> rule2)) -> rule1)) -> rule4))] @4: The cow needs the mouse.[(((((triple11 ((((triple10) -> rule2)) -> rule1)) -> rule4) triple4) -> rule5))] The mouse is red.[(((((triple11 ((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule2))] @5: The mouse needs the mouse.[(((((((triple11 ((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule2)) -> rule1))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow visits the lion.
("cow" "visits" "lion" "+")
triple2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple3
The lion needs the cow.
("lion" "needs" "cow" "+")
triple4
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple5
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple6
The mouse is round.
("mouse" "is" "round" "+")
triple7
((triple5) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple8
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple9
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple10
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple11
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple12
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple13
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple14
The squirrel is red.
("squirrel" "is" "red" "+")
((triple10) -> (rule2 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
((triple11 ((((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((((triple11 ((((triple10) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple4) -> (rule5 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int3
The squirrel is red.
("squirrel" "is" "red" "+")
int4
The mouse is red.
("mouse" "is" "red" "+")
((((triple11 ((((triple10) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int3
The squirrel is red.
("squirrel" "is" "red" "+")
int4
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((((triple11 ((((triple10) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int4
The squirrel is red.
("squirrel" "is" "red" "+")
int5