The cat is big. The cat is green. The cat is young. The cat does not see the squirrel. The cat visits the cow. The cow is red. The cow sees the cat. The mouse is blue. The mouse is not young. The mouse likes the squirrel. The mouse sees the squirrel. The squirrel is blue. The squirrel does not like the cat. The squirrel likes the cow. The squirrel likes the mouse. The squirrel visits the cow. If someone is green and they like the squirrel then they like the cow. If someone is red then they visit the mouse. If the mouse visits the cow then the cow is young. If someone visits the mouse and they are green then the mouse is green. If someone likes the cow then they are green. If the squirrel visits the cow and the cow sees the squirrel then the squirrel is young. If the squirrel is green then the squirrel is red. If someone is red and they like the cat then the cat visits the cow.
The cat is big.
("cat" "is" "big" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is young.
("cat" "is" "young" "+")
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow is red.
("cow" "is" "red" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is not young.
("mouse" "is" "young" "-")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel does not like the cat.
("squirrel" "likes" "cat" "-")
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If someone is green and they like the squirrel then they like the cow.
((("someone" "is" "green" "+") ("someone" "likes" "squirrel" "+")) -> ("someone" "likes" "cow" "+"))
If someone is red then they visit the mouse.
((("someone" "is" "red" "+")) -> ("someone" "visits" "mouse" "+"))
If the mouse visits the cow then the cow is young.
((("mouse" "visits" "cow" "+")) -> ("cow" "is" "young" "+"))
If someone visits the mouse and they are green then the mouse is green.
((("someone" "visits" "mouse" "+") ("someone" "is" "green" "+")) -> ("mouse" "is" "green" "+"))
If someone likes the cow then they are green.
((("someone" "likes" "cow" "+")) -> ("someone" "is" "green" "+"))
If the squirrel visits the cow and the cow sees the squirrel then the squirrel is young.
((("squirrel" "visits" "cow" "+") ("cow" "sees" "squirrel" "+")) -> ("squirrel" "is" "young" "+"))
If the squirrel is green then the squirrel is red.
((("squirrel" "is" "green" "+")) -> ("squirrel" "is" "red" "+"))
If someone is red and they like the cat then the cat visits the cow.
((("someone" "is" "red" "+") ("someone" "likes" "cat" "+")) -> ("cat" "visits" "cow" "+"))
The squirrel visits the cow.
True
1
proof
[(triple16)]
("squirrel" "visits" "cow" "+")
triple16
The squirrel does not like the cow.
False
1
inv-proof
[(triple14)]
("squirrel" "likes" "cow" "-")
triple14
The squirrel is green.
True
2
proof
[(((triple14) -> rule5))]
("squirrel" "is" "green" "+")
((triple14) -> (rule5 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is not green.
False
2
inv-proof
[(((triple14) -> rule5))]
("squirrel" "is" "green" "-")
((triple14) -> (rule5 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is red.
True
3
proof
[(((((triple14) -> rule5)) -> rule7))]
("squirrel" "is" "red" "+")
((((triple14) -> (rule5 % int2))) -> (rule7 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel is not red.
False
3
inv-proof
[(((((triple14) -> rule5)) -> rule7))]
("squirrel" "is" "red" "-")
((((triple14) -> (rule5 % int2))) -> (rule7 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel visits the mouse.
True
4
proof
[(((((((triple14) -> rule5)) -> rule7)) -> rule2))]
("squirrel" "visits" "mouse" "+")
((((((triple14) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The squirrel does not visit the mouse.
False
4
inv-proof
[(((((((triple14) -> rule5)) -> rule7)) -> rule2))]
("squirrel" "visits" "mouse" "-")
((((((triple14) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The mouse is green.
True
7
proof
[(((((((((triple14) -> rule5)) -> rule7)) -> rule2) ((triple14) -> rule5)) -> rule4))]
("mouse" "is" "green" "+")
((((((((triple14) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2)) ((triple14) -> (rule5 % int4))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
int4
The mouse is not green.
False
7
inv-proof
[(((((((((triple14) -> rule5)) -> rule7)) -> rule2) ((triple14) -> rule5)) -> rule4))]
("mouse" "is" "green" "-")
((((((((triple14) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2)) ((triple14) -> (rule5 % int4))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
int4
The mouse likes the cow.
True
9
proof
[(((((((((((triple14) -> rule5)) -> rule7)) -> rule2) ((triple14) -> rule5)) -> rule4) triple10) -> rule1))]
("mouse" "likes" "cow" "+")
((((((((((triple14) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule2 % int3)) ((triple14) -> (rule5 % int5))) -> (rule4 % int2)) triple10) -> (rule1 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int3
The squirrel is red.
("squirrel" "is" "red" "+")
int4
The squirrel is green.
("squirrel" "is" "green" "+")
int5
The mouse does not like the cow.
False
9
inv-proof
[(((((((((((triple14) -> rule5)) -> rule7)) -> rule2) ((triple14) -> rule5)) -> rule4) triple10) -> rule1))]
("mouse" "likes" "cow" "-")
((((((((((triple14) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule2 % int3)) ((triple14) -> (rule5 % int5))) -> (rule4 % int2)) triple10) -> (rule1 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int3
The squirrel is red.
("squirrel" "is" "red" "+")
int4
The squirrel is green.
("squirrel" "is" "green" "+")
int5
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "cow" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The cow is not green.
Unknown
inv-rconc
[@2: The cow is green.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("cow" "is" "green" "-")
The cat likes the cow.
Unknown
rconc
[@1: The cat likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "cow" "+")
The cat does not visit the mouse.
Unknown
inv-rconc
[@1: The cat visits the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "mouse" "-")
The squirrel is young.
Unknown
rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "young" "+")
The squirrel does not see the cat.
Unknown
inv-random
[@0: The squirrel sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "cat" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
The mouse does not visit the squirrel.
Unknown
inv-random
[@0: The mouse visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "squirrel" "-")
The mouse visits the cat.
Unknown
random
[@0: The mouse visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cat" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cat visits the squirrel.
Unknown
random
[@0: The cat visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "squirrel" "+")
@0: The cat does not see the squirrel.[(triple4)] The cat is big.[(triple1)] The cat is green.[(triple2)] The cat is young.[(triple3)] The cat visits the cow.[(triple5)] The cow is red.[(triple6)] The cow sees the cat.[(triple7)] The mouse is blue.[(triple8)] The mouse is not young.[(triple9)] The mouse likes the squirrel.[(triple10)] The mouse sees the squirrel.[(triple11)] The squirrel does not like the cat.[(triple13)] The squirrel is blue.[(triple12)] The squirrel likes the cow.[(triple14)] The squirrel likes the mouse.[(triple15)] The squirrel visits the cow.[(triple16)] @1: The cow visits the mouse.[(((triple6) -> rule2))] The squirrel is green.[(((triple14) -> rule5))] @2: The squirrel is red.[(((((triple14) -> rule5)) -> rule7))] @3: The squirrel visits the mouse.[(((((((triple14) -> rule5)) -> rule7)) -> rule2))] @4: The mouse is green.[(((((((((triple14) -> rule5)) -> rule7)) -> rule2) ((triple14) -> rule5)) -> rule4))] @5: The mouse likes the cow.[(((((((((((triple14) -> rule5)) -> rule7)) -> rule2) ((triple14) -> rule5)) -> rule4) triple10) -> rule1))]
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
triple4
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is young.
("cat" "is" "young" "+")
triple3
The cat visits the cow.
("cat" "visits" "cow" "+")
triple5
The cow is red.
("cow" "is" "red" "+")
triple6
The cow sees the cat.
("cow" "sees" "cat" "+")
triple7
The mouse is blue.
("mouse" "is" "blue" "+")
triple8
The mouse is not young.
("mouse" "is" "young" "-")
triple9
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple10
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple11
The squirrel does not like the cat.
("squirrel" "likes" "cat" "-")
triple13
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple12
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
triple14
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple15
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple16
The cow visits the mouse.
("cow" "visits" "mouse" "+")
((triple6) -> (rule2 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
((triple14) -> (rule5 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
((((triple14) -> (rule5 % int2))) -> (rule7 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
((((((triple14) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The mouse is green.
("mouse" "is" "green" "+")
((((((((triple14) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2)) ((triple14) -> (rule5 % int4))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
int4
The mouse likes the cow.
("mouse" "likes" "cow" "+")
((((((((((triple14) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule2 % int3)) ((triple14) -> (rule5 % int5))) -> (rule4 % int2)) triple10) -> (rule1 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int3
The squirrel is red.
("squirrel" "is" "red" "+")
int4
The squirrel is green.
("squirrel" "is" "green" "+")
int5