The bald eagle eats the cat. The bald eagle is green. The cat is green. The cat sees the lion. The lion needs the bald eagle. The rabbit needs the cat. The rabbit sees the lion. If someone is red and they need the rabbit then the rabbit needs the bald eagle. If someone eats the bald eagle then the bald eagle sees the lion. If someone needs the lion then they are green. If someone eats the bald eagle then they see the lion. If someone is green then they see the rabbit. If the cat is green and the cat sees the lion then the cat needs the rabbit. If someone sees the bald eagle then they need the lion. If someone needs the cat then they need the rabbit. If someone sees the rabbit then the rabbit sees the bald eagle.
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
The bald eagle is green.
("bald eagle" "is" "green" "+")
The cat is green.
("cat" "is" "green" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If someone is red and they need the rabbit then the rabbit needs the bald eagle.
((("someone" "is" "red" "+") ("someone" "needs" "rabbit" "+")) -> ("rabbit" "needs" "bald eagle" "+"))
If someone eats the bald eagle then the bald eagle sees the lion.
((("someone" "eats" "bald eagle" "+")) -> ("bald eagle" "sees" "lion" "+"))
If someone needs the lion then they are green.
((("someone" "needs" "lion" "+")) -> ("someone" "is" "green" "+"))
If someone eats the bald eagle then they see the lion.
((("someone" "eats" "bald eagle" "+")) -> ("someone" "sees" "lion" "+"))
If someone is green then they see the rabbit.
((("someone" "is" "green" "+")) -> ("someone" "sees" "rabbit" "+"))
If the cat is green and the cat sees the lion then the cat needs the rabbit.
((("cat" "is" "green" "+") ("cat" "sees" "lion" "+")) -> ("cat" "needs" "rabbit" "+"))
If someone sees the bald eagle then they need the lion.
((("someone" "sees" "bald eagle" "+")) -> ("someone" "needs" "lion" "+"))
If someone needs the cat then they need the rabbit.
((("someone" "needs" "cat" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone sees the rabbit then the rabbit sees the bald eagle.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "bald eagle" "+"))
The bald eagle is green.
True
1
proof
[(triple2)]
("bald eagle" "is" "green" "+")
triple2
The bald eagle does not eat the cat.
False
1
inv-proof
[(triple1)]
("bald eagle" "eats" "cat" "-")
triple1
The cat needs the rabbit.
True
3
proof
[(((triple3 triple4) -> rule6))]
("cat" "needs" "rabbit" "+")
((triple3 triple4) -> (rule6 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The bald eagle does not see the rabbit.
False
2
inv-proof
[(((triple2) -> rule5))]
("bald eagle" "sees" "rabbit" "-")
((triple2) -> (rule5 % int1))
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int1
The rabbit sees the bald eagle.
True
3
proof
[(((((triple2) -> rule5)) -> rule9) OR ((((triple3) -> rule5)) -> rule9))]
("rabbit" "sees" "bald eagle" "+")
((((triple2) -> (rule5 % int2))) -> (rule9 % int1))
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int1
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule9 % int1))
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The rabbit does not see the bald eagle.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule9) OR ((((triple3) -> rule5)) -> rule9))]
("rabbit" "sees" "bald eagle" "-")
((((triple2) -> (rule5 % int2))) -> (rule9 % int1))
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int1
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule9 % int1))
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The rabbit needs the lion.
True
4
proof
[(((((((triple2) -> rule5)) -> rule9)) -> rule7) OR ((((((triple3) -> rule5)) -> rule9)) -> rule7))]
("rabbit" "needs" "lion" "+")
((((((triple2) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int2
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int3
The rabbit does not need the lion.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule9)) -> rule7) OR ((((((triple3) -> rule5)) -> rule9)) -> rule7))]
("rabbit" "needs" "lion" "-")
((((((triple2) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int2
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int3
The rabbit is green.
True
5
proof
[(((((((((triple2) -> rule5)) -> rule9)) -> rule7)) -> rule3) OR ((((((((triple3) -> rule5)) -> rule9)) -> rule7)) -> rule3))]
("rabbit" "is" "green" "+")
((((((((triple2) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int3
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int4
((((((((triple3) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int4
The rabbit is not green.
False
5
inv-proof
[(((((((((triple2) -> rule5)) -> rule9)) -> rule7)) -> rule3) OR ((((((((triple3) -> rule5)) -> rule9)) -> rule7)) -> rule3))]
("rabbit" "is" "green" "-")
((((((((triple2) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int3
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int4
((((((((triple3) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int4
The rabbit sees the rabbit.
True
6
proof
[(((((((((((triple2) -> rule5)) -> rule9)) -> rule7)) -> rule3)) -> rule5) OR ((((((((((triple3) -> rule5)) -> rule9)) -> rule7)) -> rule3)) -> rule5))]
("rabbit" "sees" "rabbit" "+")
((((((((((triple2) -> (rule5 % int5))) -> (rule9 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int3
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int4
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int5
((((((((((triple3) -> (rule5 % int5))) -> (rule9 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int3
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int4
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int5
The rabbit does not see the rabbit.
False
6
inv-proof
[(((((((((((triple2) -> rule5)) -> rule9)) -> rule7)) -> rule3)) -> rule5) OR ((((((((((triple3) -> rule5)) -> rule9)) -> rule7)) -> rule3)) -> rule5))]
("rabbit" "sees" "rabbit" "-")
((((((((((triple2) -> (rule5 % int5))) -> (rule9 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int3
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int4
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int5
((((((((((triple3) -> (rule5 % int5))) -> (rule9 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int3
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int4
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int5
The rabbit does not need the bald eagle.
Unknown
inv-rconc
[@1: The rabbit needs the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "bald eagle" "-")
The lion needs the lion.
Unknown
rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "needs" "lion" "+")
The lion does not see the rabbit.
Unknown
inv-rconc
[@3: The lion sees the rabbit.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule7 <- FAIL)]]
("lion" "sees" "rabbit" "-")
The lion needs the rabbit.
Unknown
rconc
[@1: The lion needs the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "needs" "rabbit" "+")
The lion is not green.
Unknown
inv-rconc
[@2: The lion is green.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("lion" "is" "green" "-")
The bald eagle needs the lion.
Unknown
rconc
[@1: The bald eagle needs the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bald eagle" "needs" "lion" "+")
The bald eagle does not see the cat.
Unknown
inv-random
[@0: The bald eagle sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "cat" "-")
The bald eagle is round.
Unknown
random
[@0: The bald eagle is round.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "round" "+")
The bald eagle does not eat the lion.
Unknown
inv-random
[@0: The bald eagle eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "lion" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
The bald eagle does not eat the rabbit.
Unknown
inv-random
[@0: The bald eagle eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "rabbit" "-")
The cat sees the bald eagle.
Unknown
random
[@0: The cat sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "bald eagle" "+")
@0: The bald eagle eats the cat.[(triple1)] The bald eagle is green.[(triple2)] The cat is green.[(triple3)] The cat sees the lion.[(triple4)] The lion needs the bald eagle.[(triple5)] The rabbit needs the cat.[(triple6)] The rabbit sees the lion.[(triple7)] @1: The bald eagle sees the rabbit.[(((triple2) -> rule5))] The cat needs the rabbit.[(((triple3 triple4) -> rule6))] The cat sees the rabbit.[(((triple3) -> rule5))] The rabbit needs the rabbit.[(((triple6) -> rule8))] @2: The rabbit sees the bald eagle.[(((((triple2) -> rule5)) -> rule9) OR ((((triple3) -> rule5)) -> rule9))] @3: The rabbit needs the lion.[(((((((triple2) -> rule5)) -> rule9)) -> rule7) OR ((((((triple3) -> rule5)) -> rule9)) -> rule7))] @4: The rabbit is green.[(((((((((triple2) -> rule5)) -> rule9)) -> rule7)) -> rule3) OR ((((((((triple3) -> rule5)) -> rule9)) -> rule7)) -> rule3))] @5: The rabbit sees the rabbit.[(((((((((((triple2) -> rule5)) -> rule9)) -> rule7)) -> rule3)) -> rule5) OR ((((((((((triple3) -> rule5)) -> rule9)) -> rule7)) -> rule3)) -> rule5))]
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
triple1
The bald eagle is green.
("bald eagle" "is" "green" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat sees the lion.
("cat" "sees" "lion" "+")
triple4
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
triple5
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple6
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple7
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
((triple2) -> (rule5 % int1))
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
((triple3 triple4) -> (rule6 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
((triple3) -> (rule5 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple6) -> (rule8 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
((((triple2) -> (rule5 % int2))) -> (rule9 % int1))
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int1
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule9 % int1))
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
((((((triple2) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int2
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
((((((((triple2) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int3
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int4
((((((((triple3) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int4
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((((((((triple2) -> (rule5 % int5))) -> (rule9 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int3
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int4
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int5
((((((((((triple3) -> (rule5 % int5))) -> (rule9 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int3
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int4
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int5