The bald eagle is cold. The bald eagle needs the rabbit. The bald eagle sees the cow. The cow is red. The cow sees the bald eagle. The cow sees the tiger. The rabbit chases the cow. The rabbit is red. The rabbit is round. The rabbit needs the tiger. The tiger is round. If the cow needs the tiger then the cow sees the rabbit. If something needs the tiger then the tiger is red. If something is red then it needs the tiger. If something chases the tiger and it is big then it sees the tiger. If something sees the rabbit and it is red then it chases the cow. If something sees the rabbit and the rabbit is big then it needs the tiger. If something sees the rabbit and it needs the cow then the rabbit is cold. If something chases the cow then it needs the cow.
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
The cow is red.
("cow" "is" "red" "+")
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger is round.
("tiger" "is" "round" "+")
If the cow needs the tiger then the cow sees the rabbit.
((("cow" "needs" "tiger" "+")) -> ("cow" "sees" "rabbit" "+"))
If something needs the tiger then the tiger is red.
((("something" "needs" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If something is red then it needs the tiger.
((("something" "is" "red" "+")) -> ("something" "needs" "tiger" "+"))
If something chases the tiger and it is big then it sees the tiger.
((("something" "chases" "tiger" "+") ("something" "is" "big" "+")) -> ("something" "sees" "tiger" "+"))
If something sees the rabbit and it is red then it chases the cow.
((("something" "sees" "rabbit" "+") ("something" "is" "red" "+")) -> ("something" "chases" "cow" "+"))
If something sees the rabbit and the rabbit is big then it needs the tiger.
((("something" "sees" "rabbit" "+") ("rabbit" "is" "big" "+")) -> ("something" "needs" "tiger" "+"))
If something sees the rabbit and it needs the cow then the rabbit is cold.
((("something" "sees" "rabbit" "+") ("something" "needs" "cow" "+")) -> ("rabbit" "is" "cold" "+"))
If something chases the cow then it needs the cow.
((("something" "chases" "cow" "+")) -> ("something" "needs" "cow" "+"))
The rabbit needs the tiger.
True
1
proof
[(triple10 OR ((triple8) -> rule3))]
("rabbit" "needs" "tiger" "+")
triple10
((triple8) -> (rule3 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The cow does not see the bald eagle.
False
1
inv-proof
[(triple5)]
("cow" "sees" "bald eagle" "-")
triple5
The tiger is red.
True
2
proof
[(((triple10) -> rule2) OR ((((triple4) -> rule3)) -> rule2) OR ((((triple8) -> rule3)) -> rule2))]
("tiger" "is" "red" "+")
((triple10) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int2
The tiger is not red.
False
2
inv-proof
[(((triple10) -> rule2) OR ((((triple4) -> rule3)) -> rule2) OR ((((triple8) -> rule3)) -> rule2))]
("tiger" "is" "red" "-")
((triple10) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int2
The cow sees the rabbit.
True
3
proof
[(((((triple4) -> rule3)) -> rule1))]
("cow" "sees" "rabbit" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The tiger does not need the tiger.
False
3
inv-proof
[(((((triple10) -> rule2)) -> rule3) OR ((((((triple4) -> rule3)) -> rule2)) -> rule3) OR ((((((triple8) -> rule3)) -> rule2)) -> rule3))]
("tiger" "needs" "tiger" "-")
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
((((((triple8) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int3
The cow chases the cow.
True
5
proof
[(((((((triple4) -> rule3)) -> rule1) triple4) -> rule5))]
("cow" "chases" "cow" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule5 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
The cow does not chase the cow.
False
5
inv-proof
[(((((((triple4) -> rule3)) -> rule1) triple4) -> rule5))]
("cow" "chases" "cow" "-")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule5 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
The cow needs the cow.
True
6
proof
[(((((((((triple4) -> rule3)) -> rule1) triple4) -> rule5)) -> rule8))]
("cow" "needs" "cow" "+")
((((((((triple4) -> (rule3 % int4))) -> (rule1 % int3)) triple4) -> (rule5 % int2))) -> (rule8 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int4
The cow does not need the cow.
False
6
inv-proof
[(((((((((triple4) -> rule3)) -> rule1) triple4) -> rule5)) -> rule8))]
("cow" "needs" "cow" "-")
((((((((triple4) -> (rule3 % int4))) -> (rule1 % int3)) triple4) -> (rule5 % int2))) -> (rule8 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int4
The rabbit is cold.
True
10
proof
[(((((((triple4) -> rule3)) -> rule1) ((((((((triple4) -> rule3)) -> rule1) triple4) -> rule5)) -> rule8)) -> rule7))]
("rabbit" "is" "cold" "+")
((((((triple4) -> (rule3 % int5))) -> (rule1 % int4)) ((((((((triple4) -> (rule3 % int5))) -> (rule1 % int4)) triple4) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int5
The rabbit is not cold.
False
10
inv-proof
[(((((((triple4) -> rule3)) -> rule1) ((((((((triple4) -> rule3)) -> rule1) triple4) -> rule5)) -> rule8)) -> rule7))]
("rabbit" "is" "cold" "-")
((((((triple4) -> (rule3 % int5))) -> (rule1 % int4)) ((((((((triple4) -> (rule3 % int5))) -> (rule1 % int4)) triple4) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int5
The rabbit does not see the tiger.
Unknown
inv-rconc
[@1: The rabbit sees the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "sees" "tiger" "-")
The bald eagle chases the cow.
Unknown
rconc
[@1: The bald eagle chases the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "chases" "cow" "+")
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The bald eagle needs the tiger.
Unknown
rconc
[@1: The bald eagle needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "needs" "tiger" "+")
The bald eagle does not need the cow.
Unknown
inv-rconc
[@2: The bald eagle needs the cow.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("bald eagle" "needs" "cow" "-")
The bald eagle sees the tiger.
Unknown
rconc
[@1: The bald eagle sees the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "sees" "tiger" "+")
The bald eagle does not chase the bald eagle.
Unknown
inv-random
[@0: The bald eagle chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "bald eagle" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
The bald eagle is not red.
Unknown
inv-random
[@0: The bald eagle is red.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "red" "-")
The bald eagle needs the bald eagle.
Unknown
random
[@0: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "bald eagle" "+")
The bald eagle is not big.
Unknown
inv-random
[@0: The bald eagle is big.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "big" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
@0: The bald eagle is cold.[(triple1)] The bald eagle needs the rabbit.[(triple2)] The bald eagle sees the cow.[(triple3)] The cow is red.[(triple4)] The cow sees the bald eagle.[(triple5)] The cow sees the tiger.[(triple6)] The rabbit chases the cow.[(triple7)] The rabbit is red.[(triple8)] The rabbit is round.[(triple9)] The rabbit needs the tiger.[(triple10 OR ((triple8) -> rule3))] The tiger is round.[(triple11)] @1: The cow needs the tiger.[(((triple4) -> rule3))] The rabbit needs the cow.[(((triple7) -> rule8))] The tiger is red.[(((triple10) -> rule2) OR ((((triple4) -> rule3)) -> rule2) OR ((((triple8) -> rule3)) -> rule2))] @2: The cow sees the rabbit.[(((((triple4) -> rule3)) -> rule1))] The tiger needs the tiger.[(((((triple10) -> rule2)) -> rule3) OR ((((((triple4) -> rule3)) -> rule2)) -> rule3) OR ((((((triple8) -> rule3)) -> rule2)) -> rule3))] @3: The cow chases the cow.[(((((((triple4) -> rule3)) -> rule1) triple4) -> rule5))] @4: The cow needs the cow.[(((((((((triple4) -> rule3)) -> rule1) triple4) -> rule5)) -> rule8))] @5: The rabbit is cold.[(((((((triple4) -> rule3)) -> rule1) ((((((((triple4) -> rule3)) -> rule1) triple4) -> rule5)) -> rule8)) -> rule7))]
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple1
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
triple2
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
triple5
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple6
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple7
The rabbit is red.
("rabbit" "is" "red" "+")
triple8
The rabbit is round.
("rabbit" "is" "round" "+")
triple9
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple10
((triple8) -> (rule3 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
triple11
The cow needs the tiger.
("cow" "needs" "tiger" "+")
((triple4) -> (rule3 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
((triple7) -> (rule8 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
((triple10) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
((((((triple8) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int3
The cow chases the cow.
("cow" "chases" "cow" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule5 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
The cow needs the cow.
("cow" "needs" "cow" "+")
((((((((triple4) -> (rule3 % int4))) -> (rule1 % int3)) triple4) -> (rule5 % int2))) -> (rule8 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int4
The rabbit is cold.
("rabbit" "is" "cold" "+")
((((((triple4) -> (rule3 % int5))) -> (rule1 % int4)) ((((((((triple4) -> (rule3 % int5))) -> (rule1 % int4)) triple4) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int5