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