The bear is green. The bear needs the cat. The cat is red. The cat needs the lion. The cat sees the bear. The cat sees the lion. The lion eats the bear. The lion is cold. The rabbit is green. The rabbit sees the lion. If something sees the lion then the lion is red. If something sees the rabbit and it eats the rabbit then the rabbit needs the lion. If something needs the lion then it eats the lion. If something is red then it is green. Green things are round. If something needs the lion and the lion eats the rabbit then the rabbit is green. If something is round then it needs the lion.
The bear is green.
("bear" "is" "green" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The cat is red.
("cat" "is" "red" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The lion is cold.
("lion" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If something sees the lion then the lion is red.
((("something" "sees" "lion" "+")) -> ("lion" "is" "red" "+"))
If something sees the rabbit and it eats the rabbit then the rabbit needs the lion.
((("something" "sees" "rabbit" "+") ("something" "eats" "rabbit" "+")) -> ("rabbit" "needs" "lion" "+"))
If something needs the lion then it eats the lion.
((("something" "needs" "lion" "+")) -> ("something" "eats" "lion" "+"))
If something is red then it is green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something needs the lion and the lion eats the rabbit then the rabbit is green.
((("something" "needs" "lion" "+") ("lion" "eats" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If something is round then it needs the lion.
((("something" "is" "round" "+")) -> ("something" "needs" "lion" "+"))
The cat is red.
True
1
proof
[(triple3)]
("cat" "is" "red" "+")
triple3
The rabbit does not see the lion.
False
1
inv-proof
[(triple10)]
("rabbit" "sees" "lion" "-")
triple10
The rabbit is round.
True
2
proof
[(((triple9) -> rule5))]
("rabbit" "is" "round" "+")
((triple9) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The cat is not green.
False
2
inv-proof
[(((triple3) -> rule4))]
("cat" "is" "green" "-")
((triple3) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The lion is green.
True
3
proof
[(((((triple10) -> rule1)) -> rule4) OR ((((triple6) -> rule1)) -> rule4))]
("lion" "is" "green" "+")
((((triple10) -> (rule1 % int2))) -> (rule4 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule4 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The bear does not need the lion.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule7))]
("bear" "needs" "lion" "-")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear eats the lion.
True
4
proof
[(((((((triple1) -> rule5)) -> rule7)) -> rule3))]
("bear" "eats" "lion" "+")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear eats the lion.
("bear" "eats" "lion" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The lion is not round.
False
4
inv-proof
[(((((((triple10) -> rule1)) -> rule4)) -> rule5) OR ((((((triple6) -> rule1)) -> rule4)) -> rule5))]
("lion" "is" "round" "-")
((((((triple10) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
((((((triple6) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The lion needs the lion.
True
5
proof
[(((((((((triple10) -> rule1)) -> rule4)) -> rule5)) -> rule7) OR ((((((((triple6) -> rule1)) -> rule4)) -> rule5)) -> rule7))]
("lion" "needs" "lion" "+")
((((((((triple10) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
((((((((triple6) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The lion does not need the lion.
False
5
inv-proof
[(((((((((triple10) -> rule1)) -> rule4)) -> rule5)) -> rule7) OR ((((((((triple6) -> rule1)) -> rule4)) -> rule5)) -> rule7))]
("lion" "needs" "lion" "-")
((((((((triple10) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
((((((((triple6) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The lion eats the lion.
True
6
proof
[(((((((((((triple10) -> rule1)) -> rule4)) -> rule5)) -> rule7)) -> rule3) OR ((((((((((triple6) -> rule1)) -> rule4)) -> rule5)) -> rule7)) -> rule3))]
("lion" "eats" "lion" "+")
((((((((((triple10) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion is green.
("lion" "is" "green" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
((((((((((triple6) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion is green.
("lion" "is" "green" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
The lion does not eat the lion.
False
6
inv-proof
[(((((((((((triple10) -> rule1)) -> rule4)) -> rule5)) -> rule7)) -> rule3) OR ((((((((((triple6) -> rule1)) -> rule4)) -> rule5)) -> rule7)) -> rule3))]
("lion" "eats" "lion" "-")
((((((((((triple10) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion is green.
("lion" "is" "green" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
((((((((((triple6) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion is green.
("lion" "is" "green" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
The rabbit does not see the cat.
Unknown
inv-random
[@0: The rabbit sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "cat" "-")
The lion needs the cat.
Unknown
random
[@0: The lion needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cat" "+")
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 rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
The rabbit does not need the cat.
Unknown
inv-random
[@0: The rabbit needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "cat" "-")
The bear eats the cat.
Unknown
random
[@0: The bear eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "cat" "+")
The rabbit does not eat the bear.
Unknown
inv-random
[@0: The rabbit eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "bear" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The rabbit does not need the bear.
Unknown
inv-random
[@0: The rabbit needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "bear" "-")
The bear eats the rabbit.
Unknown
random
[@0: The bear eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "rabbit" "+")
The bear does not see the lion.
Unknown
inv-random
[@0: The bear sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "lion" "-")
The lion sees the bear.
Unknown
random
[@0: The lion sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "bear" "+")
@0: The bear is green.[(triple1)] The bear needs the cat.[(triple2)] The cat is red.[(triple3)] The cat needs the lion.[(triple4 OR ((((((triple3) -> rule4)) -> rule5)) -> rule7))] The cat sees the bear.[(triple5)] The cat sees the lion.[(triple6)] The lion eats the bear.[(triple7)] The lion is cold.[(triple8)] The rabbit is green.[(triple9)] The rabbit sees the lion.[(triple10)] @1: The bear is round.[(((triple1) -> rule5))] The cat eats the lion.[(((triple4) -> rule3) OR ((((((((triple3) -> rule4)) -> rule5)) -> rule7)) -> rule3))] The cat is green.[(((triple3) -> rule4))] The lion is red.[(((triple10) -> rule1) OR ((triple6) -> rule1))] The rabbit is round.[(((triple9) -> rule5))] @2: The bear needs the lion.[(((((triple1) -> rule5)) -> rule7))] The cat is round.[(((((triple3) -> rule4)) -> rule5))] The lion is green.[(((((triple10) -> rule1)) -> rule4) OR ((((triple6) -> rule1)) -> rule4))] The rabbit needs the lion.[(((((triple9) -> rule5)) -> rule7))] @3: The bear eats the lion.[(((((((triple1) -> rule5)) -> rule7)) -> rule3))] The lion is round.[(((((((triple10) -> rule1)) -> rule4)) -> rule5) OR ((((((triple6) -> rule1)) -> rule4)) -> rule5))] The rabbit eats the lion.[(((((((triple9) -> rule5)) -> rule7)) -> rule3))] @4: The lion needs the lion.[(((((((((triple10) -> rule1)) -> rule4)) -> rule5)) -> rule7) OR ((((((((triple6) -> rule1)) -> rule4)) -> rule5)) -> rule7))] @5: The lion eats the lion.[(((((((((((triple10) -> rule1)) -> rule4)) -> rule5)) -> rule7)) -> rule3) OR ((((((((((triple6) -> rule1)) -> rule4)) -> rule5)) -> rule7)) -> rule3))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear needs the cat.
("bear" "needs" "cat" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat needs the lion.
("cat" "needs" "lion" "+")
triple4
((((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
The cat sees the bear.
("cat" "sees" "bear" "+")
triple5
The cat sees the lion.
("cat" "sees" "lion" "+")
triple6
The lion eats the bear.
("lion" "eats" "bear" "+")
triple7
The lion is cold.
("lion" "is" "cold" "+")
triple8
The rabbit is green.
("rabbit" "is" "green" "+")
triple9
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple10
The bear is round.
("bear" "is" "round" "+")
((triple1) -> (rule5 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
((triple4) -> (rule3 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
((((((((triple3) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat is green.
("cat" "is" "green" "+")
int4
The cat is green.
("cat" "is" "green" "+")
((triple3) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The lion is red.
("lion" "is" "red" "+")
((triple10) -> (rule1 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((triple6) -> (rule1 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple9) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The cat is round.
("cat" "is" "round" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The lion is green.
("lion" "is" "green" "+")
((((triple10) -> (rule1 % int2))) -> (rule4 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule4 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
((((triple9) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The bear eats the lion.
("bear" "eats" "lion" "+")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear eats the lion.
("bear" "eats" "lion" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The lion is round.
("lion" "is" "round" "+")
((((((triple10) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
((((((triple6) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
((((((triple9) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The lion needs the lion.
("lion" "needs" "lion" "+")
((((((((triple10) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
((((((((triple6) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The lion eats the lion.
("lion" "eats" "lion" "+")
((((((((((triple10) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion is green.
("lion" "is" "green" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
((((((((((triple6) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion is green.
("lion" "is" "green" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5