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