The cow eats the lion. The lion is blue. The lion is red. If something is big then it eats the lion. If something is red then it eats the cow. If something eats the lion then the lion needs the cow. If something likes the lion and the lion is red then the lion likes the cow. If something eats the lion and it needs the cow then the lion is green. If something is blue and it eats the cow then it eats the lion. If something is nice and red then it eats the cow. If something likes the lion and it is big then it needs the lion.
The cow eats the lion.
("cow" "eats" "lion" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is red.
("lion" "is" "red" "+")
If something is big then it eats the lion.
((("something" "is" "big" "+")) -> ("something" "eats" "lion" "+"))
If something is red then it eats the cow.
((("something" "is" "red" "+")) -> ("something" "eats" "cow" "+"))
If something eats the lion then the lion needs the cow.
((("something" "eats" "lion" "+")) -> ("lion" "needs" "cow" "+"))
If something likes the lion and the lion is red then the lion likes the cow.
((("something" "likes" "lion" "+") ("lion" "is" "red" "+")) -> ("lion" "likes" "cow" "+"))
If something eats the lion and it needs the cow then the lion is green.
((("something" "eats" "lion" "+") ("something" "needs" "cow" "+")) -> ("lion" "is" "green" "+"))
If something is blue and it eats the cow then it eats the lion.
((("something" "is" "blue" "+") ("something" "eats" "cow" "+")) -> ("something" "eats" "lion" "+"))
If something is nice and red then it eats the cow.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "eats" "cow" "+"))
If something likes the lion and it is big then it needs the lion.
((("something" "likes" "lion" "+") ("something" "is" "big" "+")) -> ("something" "needs" "lion" "+"))
The lion is blue.
True
1
proof
[(triple2)]
("lion" "is" "blue" "+")
triple2
The cow does not eat the lion.
False
1
inv-proof
[(triple1)]
("cow" "eats" "lion" "-")
triple1
The lion needs the cow.
True
2
proof
[(((triple1) -> rule3) OR ((((triple2 ((triple3) -> rule2)) -> rule6)) -> rule3))]
("lion" "needs" "cow" "+")
((triple1) -> (rule3 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
((((triple2 ((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the cow.
("lion" "eats" "cow" "+")
int3
The lion does not need the cow.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((triple2 ((triple3) -> rule2)) -> rule6)) -> rule3))]
("lion" "needs" "cow" "-")
((triple1) -> (rule3 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
((((triple2 ((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the cow.
("lion" "eats" "cow" "+")
int3
The lion eats the lion.
True
4
proof
[(((triple2 ((triple3) -> rule2)) -> rule6))]
("lion" "eats" "lion" "+")
((triple2 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The lion does not eat the lion.
False
4
inv-proof
[(((triple2 ((triple3) -> rule2)) -> rule6))]
("lion" "eats" "lion" "-")
((triple2 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The lion is green.
True
7
proof
[(((((triple2 ((triple3) -> rule2)) -> rule6) ((triple1) -> rule3)) -> rule5) OR ((((triple2 ((triple3) -> rule2)) -> rule6) ((((triple2 ((triple3) -> rule2)) -> rule6)) -> rule3)) -> rule5))]
("lion" "is" "green" "+")
((((triple2 ((triple3) -> (rule2 % int4))) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The lion eats the cow.
("lion" "eats" "cow" "+")
int4
((((triple2 ((triple3) -> (rule2 % int4))) -> (rule6 % int3)) ((((triple2 ((triple3) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The lion eats the cow.
("lion" "eats" "cow" "+")
int4
The lion is not green.
False
7
inv-proof
[(((((triple2 ((triple3) -> rule2)) -> rule6) ((triple1) -> rule3)) -> rule5) OR ((((triple2 ((triple3) -> rule2)) -> rule6) ((((triple2 ((triple3) -> rule2)) -> rule6)) -> rule3)) -> rule5))]
("lion" "is" "green" "-")
((((triple2 ((triple3) -> (rule2 % int4))) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The lion eats the cow.
("lion" "eats" "cow" "+")
int4
((((triple2 ((triple3) -> (rule2 % int4))) -> (rule6 % int3)) ((((triple2 ((triple3) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The lion eats the cow.
("lion" "eats" "cow" "+")
int4
The cow does not need the lion.
Unknown
inv-rconc
[@1: The cow needs the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "needs" "lion" "-")
The lion needs the lion.
Unknown
rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "needs" "lion" "+")
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "eats" "cow" "-")
The lion likes the cow.
Unknown
rconc
[@1: The lion likes the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "likes" "cow" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The cow eats the lion.[(triple1)] The lion is blue.[(triple2)] The lion is red.[(triple3)] @1: The lion eats the cow.[(((triple3) -> rule2))] The lion needs the cow.[(((triple1) -> rule3) OR ((((triple2 ((triple3) -> rule2)) -> rule6)) -> rule3))] @2: The lion eats the lion.[(((triple2 ((triple3) -> rule2)) -> rule6))] @3: The lion is green.[(((((triple2 ((triple3) -> rule2)) -> rule6) ((triple1) -> rule3)) -> rule5) OR ((((triple2 ((triple3) -> rule2)) -> rule6) ((((triple2 ((triple3) -> rule2)) -> rule6)) -> rule3)) -> rule5))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The lion is blue.
("lion" "is" "blue" "+")
triple2
The lion is red.
("lion" "is" "red" "+")
triple3
The lion eats the cow.
("lion" "eats" "cow" "+")
((triple3) -> (rule2 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
((triple1) -> (rule3 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
((((triple2 ((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the cow.
("lion" "eats" "cow" "+")
int3
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple2 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The lion is green.
("lion" "is" "green" "+")
((((triple2 ((triple3) -> (rule2 % int4))) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The lion eats the cow.
("lion" "eats" "cow" "+")
int4
((((triple2 ((triple3) -> (rule2 % int4))) -> (rule6 % int3)) ((((triple2 ((triple3) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The lion eats the cow.
("lion" "eats" "cow" "+")
int4