The cat is young. The cat visits the tiger. The mouse is red. The mouse likes the squirrel. The mouse sees the squirrel. The squirrel sees the tiger. The squirrel visits the mouse. The squirrel visits the tiger. The tiger is red. The tiger likes the cat. If something visits the mouse and it likes the squirrel then it visits the squirrel. If something likes the squirrel then it is young. If something likes the cat then it is kind. If something is kind and red then it visits the mouse. If something sees the squirrel then it likes the cat. If something likes the squirrel then the squirrel sees the tiger. If something likes the tiger and it is kind then the tiger visits the cat. If something visits the squirrel and it visits the mouse then it sees the mouse. If something sees the cat and it visits the cat then it sees the squirrel.
The cat is young.
("cat" "is" "young" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If something visits the mouse and it likes the squirrel then it visits the squirrel.
((("something" "visits" "mouse" "+") ("something" "likes" "squirrel" "+")) -> ("something" "visits" "squirrel" "+"))
If something likes the squirrel then it is young.
((("something" "likes" "squirrel" "+")) -> ("something" "is" "young" "+"))
If something likes the cat then it is kind.
((("something" "likes" "cat" "+")) -> ("something" "is" "kind" "+"))
If something is kind and red then it visits the mouse.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "visits" "mouse" "+"))
If something sees the squirrel then it likes the cat.
((("something" "sees" "squirrel" "+")) -> ("something" "likes" "cat" "+"))
If something likes the squirrel then the squirrel sees the tiger.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "sees" "tiger" "+"))
If something likes the tiger and it is kind then the tiger visits the cat.
((("something" "likes" "tiger" "+") ("something" "is" "kind" "+")) -> ("tiger" "visits" "cat" "+"))
If something visits the squirrel and it visits the mouse then it sees the mouse.
((("something" "visits" "squirrel" "+") ("something" "visits" "mouse" "+")) -> ("something" "sees" "mouse" "+"))
If something sees the cat and it visits the cat then it sees the squirrel.
((("something" "sees" "cat" "+") ("something" "visits" "cat" "+")) -> ("something" "sees" "squirrel" "+"))
The tiger likes the cat.
True
1
proof
[(triple10)]
("tiger" "likes" "cat" "+")
triple10
The tiger does not like the cat.
False
1
inv-proof
[(triple10)]
("tiger" "likes" "cat" "-")
triple10
The tiger is kind.
True
2
proof
[(((triple10) -> rule3))]
("tiger" "is" "kind" "+")
((triple10) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The mouse does not like the cat.
False
2
inv-proof
[(((triple5) -> rule5))]
("mouse" "likes" "cat" "-")
((triple5) -> (rule5 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The tiger visits the mouse.
True
4
proof
[(((((triple10) -> rule3) triple9) -> rule4))]
("tiger" "visits" "mouse" "+")
((((triple10) -> (rule3 % int2)) triple9) -> (rule4 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger does not visit the mouse.
False
4
inv-proof
[(((((triple10) -> rule3) triple9) -> rule4))]
("tiger" "visits" "mouse" "-")
((((triple10) -> (rule3 % int2)) triple9) -> (rule4 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The mouse visits the mouse.
True
5
proof
[(((((((triple5) -> rule5)) -> rule3) triple3) -> rule4))]
("mouse" "visits" "mouse" "+")
((((((triple5) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule4 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int3
The mouse does not visit the mouse.
False
5
inv-proof
[(((((((triple5) -> rule5)) -> rule3) triple3) -> rule4))]
("mouse" "visits" "mouse" "-")
((((((triple5) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule4 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int3
The mouse visits the squirrel.
True
7
proof
[(((((((((triple5) -> rule5)) -> rule3) triple3) -> rule4) triple4) -> rule1))]
("mouse" "visits" "squirrel" "+")
((((((((triple5) -> (rule5 % int4))) -> (rule3 % int3)) triple3) -> (rule4 % int2)) triple4) -> (rule1 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int4
The mouse does not visit the squirrel.
False
7
inv-proof
[(((((((((triple5) -> rule5)) -> rule3) triple3) -> rule4) triple4) -> rule1))]
("mouse" "visits" "squirrel" "-")
((((((((triple5) -> (rule5 % int4))) -> (rule3 % int3)) triple3) -> (rule4 % int2)) triple4) -> (rule1 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int4
The mouse sees the mouse.
True
13
proof
[(((((((((((triple5) -> rule5)) -> rule3) triple3) -> rule4) triple4) -> rule1) ((((((triple5) -> rule5)) -> rule3) triple3) -> rule4)) -> rule8))]
("mouse" "sees" "mouse" "+")
((((((((((triple5) -> (rule5 % int5))) -> (rule3 % int4)) triple3) -> (rule4 % int3)) triple4) -> (rule1 % int2)) ((((((triple5) -> (rule5 % int5))) -> (rule3 % int4)) triple3) -> (rule4 % int3))) -> (rule8 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int5
The mouse does not see the mouse.
False
13
inv-proof
[(((((((((((triple5) -> rule5)) -> rule3) triple3) -> rule4) triple4) -> rule1) ((((((triple5) -> rule5)) -> rule3) triple3) -> rule4)) -> rule8))]
("mouse" "sees" "mouse" "-")
((((((((((triple5) -> (rule5 % int5))) -> (rule3 % int4)) triple3) -> (rule4 % int3)) triple4) -> (rule1 % int2)) ((((((triple5) -> (rule5 % int5))) -> (rule3 % int4)) triple3) -> (rule4 % int3))) -> (rule8 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int5
The cat does not visit the squirrel.
Unknown
inv-rconc
[@1: The cat visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "visits" "squirrel" "-")
The tiger visits the squirrel.
Unknown
rconc
[@1: The tiger visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "squirrel" "+")
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "young" "-")
The tiger sees the squirrel.
Unknown
rconc
[@1: The tiger sees the squirrel.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("tiger" "sees" "squirrel" "+")
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
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 cat.
Unknown
inv-random
[@0: The squirrel visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "cat" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The cat likes the squirrel.
Unknown
random
[@0: The cat likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "squirrel" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is young.[(triple1)] The cat visits the tiger.[(triple2)] The mouse is red.[(triple3)] The mouse likes the squirrel.[(triple4)] The mouse sees the squirrel.[(triple5)] The squirrel sees the tiger.[(triple6 OR ((triple4) -> rule6))] The squirrel visits the mouse.[(triple7)] The squirrel visits the tiger.[(triple8)] The tiger is red.[(triple9)] The tiger likes the cat.[(triple10)] @1: The mouse is young.[(((triple4) -> rule2))] The mouse likes the cat.[(((triple5) -> rule5))] The tiger is kind.[(((triple10) -> rule3))] @2: The mouse is kind.[(((((triple5) -> rule5)) -> rule3))] The tiger visits the mouse.[(((((triple10) -> rule3) triple9) -> rule4))] @3: The mouse visits the mouse.[(((((((triple5) -> rule5)) -> rule3) triple3) -> rule4))] @4: The mouse visits the squirrel.[(((((((((triple5) -> rule5)) -> rule3) triple3) -> rule4) triple4) -> rule1))] @5: The mouse sees the mouse.[(((((((((((triple5) -> rule5)) -> rule3) triple3) -> rule4) triple4) -> rule1) ((((((triple5) -> rule5)) -> rule3) triple3) -> rule4)) -> rule8))]
The cat is young.
("cat" "is" "young" "+")
triple1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple2
The mouse is red.
("mouse" "is" "red" "+")
triple3
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple4
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple5
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple6
((triple4) -> (rule6 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple7
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple8
The tiger is red.
("tiger" "is" "red" "+")
triple9
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple10
The mouse is young.
("mouse" "is" "young" "+")
((triple4) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
((triple5) -> (rule5 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple10) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
((((triple10) -> (rule3 % int2)) triple9) -> (rule4 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((((((triple5) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule4 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int3
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
((((((((triple5) -> (rule5 % int4))) -> (rule3 % int3)) triple3) -> (rule4 % int2)) triple4) -> (rule1 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int4
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((((((((triple5) -> (rule5 % int5))) -> (rule3 % int4)) triple3) -> (rule4 % int3)) triple4) -> (rule1 % int2)) ((((((triple5) -> (rule5 % int5))) -> (rule3 % int4)) triple3) -> (rule4 % int3))) -> (rule8 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int5