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