The cow is cold. The dog is young. The dog sees the cow. The dog visits the cow. The rabbit does not eat the dog. The rabbit does not eat the squirrel. The rabbit is cold. The rabbit visits the squirrel. The squirrel is cold. The squirrel is not round. If someone visits the squirrel then the squirrel eats the rabbit. If someone eats the cow then the cow sees the dog. If the dog sees the cow and the dog eats the cow then the cow does not eat the dog. If someone is round and red then they eat the cow. If someone eats the rabbit then they eat the cow. If someone visits the rabbit then the rabbit visits the dog. If someone sees the dog then they eat the rabbit. If someone sees the squirrel and the squirrel sees the cow then the cow sees the squirrel. If someone eats the squirrel and they see the squirrel then the squirrel does not see the dog.
The cow is cold.
("cow" "is" "cold" "+")
The dog is young.
("dog" "is" "young" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The rabbit does not eat the dog.
("rabbit" "eats" "dog" "-")
The rabbit does not eat the squirrel.
("rabbit" "eats" "squirrel" "-")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is not round.
("squirrel" "is" "round" "-")
If someone visits the squirrel then the squirrel eats the rabbit.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "eats" "rabbit" "+"))
If someone eats the cow then the cow sees the dog.
((("someone" "eats" "cow" "+")) -> ("cow" "sees" "dog" "+"))
If the dog sees the cow and the dog eats the cow then the cow does not eat the dog.
((("dog" "sees" "cow" "+") ("dog" "eats" "cow" "+")) -> ("cow" "eats" "dog" "-"))
If someone is round and red then they eat the cow.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "eats" "cow" "+"))
If someone eats the rabbit then they eat the cow.
((("someone" "eats" "rabbit" "+")) -> ("someone" "eats" "cow" "+"))
If someone visits the rabbit then the rabbit visits the dog.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "visits" "dog" "+"))
If someone sees the dog then they eat the rabbit.
((("someone" "sees" "dog" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone sees the squirrel and the squirrel sees the cow then the cow sees the squirrel.
((("someone" "sees" "squirrel" "+") ("squirrel" "sees" "cow" "+")) -> ("cow" "sees" "squirrel" "+"))
If someone eats the squirrel and they see the squirrel then the squirrel does not see the dog.
((("someone" "eats" "squirrel" "+") ("someone" "sees" "squirrel" "+")) -> ("squirrel" "sees" "dog" "-"))
The squirrel is not round.
True
1
proof
[(triple10)]
("squirrel" "is" "round" "-")
triple10
The squirrel is not cold.
False
1
inv-proof
[(triple9)]
("squirrel" "is" "cold" "-")
triple9
The squirrel eats the rabbit.
True
2
proof
[(((triple8) -> rule1))]
("squirrel" "eats" "rabbit" "+")
((triple8) -> (rule1 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel does not eat the rabbit.
False
2
inv-proof
[(((triple8) -> rule1))]
("squirrel" "eats" "rabbit" "-")
((triple8) -> (rule1 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel eats the cow.
True
3
proof
[(((((triple8) -> rule1)) -> rule5))]
("squirrel" "eats" "cow" "+")
((((triple8) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int2
The squirrel does not eat the cow.
False
3
inv-proof
[(((((triple8) -> rule1)) -> rule5))]
("squirrel" "eats" "cow" "-")
((((triple8) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int2
The cow sees the dog.
True
4
proof
[(((((((triple8) -> rule1)) -> rule5)) -> rule2))]
("cow" "sees" "dog" "+")
((((((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int2
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int3
The cow does not see the dog.
False
4
inv-proof
[(((((((triple8) -> rule1)) -> rule5)) -> rule2))]
("cow" "sees" "dog" "-")
((((((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int2
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int3
The cow eats the rabbit.
True
5
proof
[(((((((((triple8) -> rule1)) -> rule5)) -> rule2)) -> rule7))]
("cow" "eats" "rabbit" "+")
((((((((triple8) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int4
The cow does not eat the rabbit.
False
5
inv-proof
[(((((((((triple8) -> rule1)) -> rule5)) -> rule2)) -> rule7))]
("cow" "eats" "rabbit" "-")
((((((((triple8) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int4
The cow eats the cow.
True
6
proof
[(((((((((((triple8) -> rule1)) -> rule5)) -> rule2)) -> rule7)) -> rule5))]
("cow" "eats" "cow" "+")
((((((((((triple8) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int4
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int5
The cow does not eat the cow.
False
6
inv-proof
[(((((((((((triple8) -> rule1)) -> rule5)) -> rule2)) -> rule7)) -> rule5))]
("cow" "eats" "cow" "-")
((((((((((triple8) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int4
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int5
The cow does not see the squirrel.
Unknown
inv-rconc
[@1: The cow sees the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "sees" "squirrel" "-")
The rabbit eats the rabbit.
Unknown
rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "eats" "rabbit" "+")
The rabbit does not visit the dog.
Unknown
inv-rconc
[@1: The rabbit visits the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "visits" "dog" "-")
The rabbit eats the cow.
Unknown
rconc
[@2: The rabbit eats the cow.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("rabbit" "eats" "cow" "+")
The dog does not eat the rabbit.
Unknown
inv-rconc
[@1: The dog eats the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "eats" "rabbit" "-")
The dog eats the cow.
Unknown
rconc
[@2: The dog eats the cow.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("dog" "eats" "cow" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The dog visits the squirrel.
Unknown
random
[@0: The dog visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "squirrel" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The squirrel visits the dog.
Unknown
random
[@0: The squirrel visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "dog" "+")
The rabbit does not see the cow.
Unknown
inv-random
[@0: The rabbit sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "cow" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
@0: The cow is cold.[(triple1)] The dog is young.[(triple2)] The dog sees the cow.[(triple3)] The dog visits the cow.[(triple4)] The rabbit does not eat the dog.[(triple5)] The rabbit does not eat the squirrel.[(triple6)] The rabbit is cold.[(triple7)] The rabbit visits the squirrel.[(triple8)] The squirrel is cold.[(triple9)] The squirrel is not round.[(triple10)] @1: The squirrel eats the rabbit.[(((triple8) -> rule1))] @2: The squirrel eats the cow.[(((((triple8) -> rule1)) -> rule5))] @3: The cow sees the dog.[(((((((triple8) -> rule1)) -> rule5)) -> rule2))] @4: The cow eats the rabbit.[(((((((((triple8) -> rule1)) -> rule5)) -> rule2)) -> rule7))] @5: The cow eats the cow.[(((((((((((triple8) -> rule1)) -> rule5)) -> rule2)) -> rule7)) -> rule5))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The dog is young.
("dog" "is" "young" "+")
triple2
The dog sees the cow.
("dog" "sees" "cow" "+")
triple3
The dog visits the cow.
("dog" "visits" "cow" "+")
triple4
The rabbit does not eat the dog.
("rabbit" "eats" "dog" "-")
triple5
The rabbit does not eat the squirrel.
("rabbit" "eats" "squirrel" "-")
triple6
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple7
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple8
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
The squirrel is not round.
("squirrel" "is" "round" "-")
triple10
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
((triple8) -> (rule1 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
((((triple8) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
((((((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int2
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int3
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
((((((((triple8) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int4
The cow eats the cow.
("cow" "eats" "cow" "+")
((((((((((triple8) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int4
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int5