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