The cat is rough. The cat is not young. The cat visits the squirrel. The lion chases the mouse. The lion does not visit the mouse. The mouse is kind. The mouse is rough. The squirrel is kind. The squirrel is round. The squirrel is young. If something likes the squirrel then it visits the mouse. If the squirrel is round then the squirrel is rough. If something is kind and it chases the mouse then the mouse visits the squirrel. If something is round then it likes the squirrel. If the mouse chases the squirrel then the mouse chases the lion. If something visits the mouse and it is rough then the mouse is round.
The cat is rough.
("cat" "is" "rough" "+")
The cat is not young.
("cat" "is" "young" "-")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
If something likes the squirrel then it visits the mouse.
((("something" "likes" "squirrel" "+")) -> ("something" "visits" "mouse" "+"))
If the squirrel is round then the squirrel is rough.
((("squirrel" "is" "round" "+")) -> ("squirrel" "is" "rough" "+"))
If something is kind and it chases the mouse then the mouse visits the squirrel.
((("something" "is" "kind" "+") ("something" "chases" "mouse" "+")) -> ("mouse" "visits" "squirrel" "+"))
If something is round then it likes the squirrel.
((("something" "is" "round" "+")) -> ("something" "likes" "squirrel" "+"))
If the mouse chases the squirrel then the mouse chases the lion.
((("mouse" "chases" "squirrel" "+")) -> ("mouse" "chases" "lion" "+"))
If something visits the mouse and it is rough then the mouse is round.
((("something" "visits" "mouse" "+") ("something" "is" "rough" "+")) -> ("mouse" "is" "round" "+"))
The lion does not visit the mouse.
True
1
proof
[(triple5)]
("lion" "visits" "mouse" "-")
triple5
The squirrel is not kind.
False
1
inv-proof
[(triple8)]
("squirrel" "is" "kind" "-")
triple8
The squirrel is rough.
True
2
proof
[(((triple9) -> rule2))]
("squirrel" "is" "rough" "+")
((triple9) -> (rule2 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is not rough.
False
2
inv-proof
[(((triple9) -> rule2))]
("squirrel" "is" "rough" "-")
((triple9) -> (rule2 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel visits the mouse.
True
3
proof
[(((((triple9) -> rule4)) -> rule1))]
("squirrel" "visits" "mouse" "+")
((((triple9) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2
The squirrel does not visit the mouse.
False
3
inv-proof
[(((((triple9) -> rule4)) -> rule1))]
("squirrel" "visits" "mouse" "-")
((((triple9) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2
The mouse is round.
True
6
proof
[(((((((triple9) -> rule4)) -> rule1) ((triple9) -> rule2)) -> rule6))]
("mouse" "is" "round" "+")
((((((triple9) -> (rule4 % int4))) -> (rule1 % int3)) ((triple9) -> (rule2 % int2))) -> (rule6 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int3
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int4
The mouse is not round.
False
6
inv-proof
[(((((((triple9) -> rule4)) -> rule1) ((triple9) -> rule2)) -> rule6))]
("mouse" "is" "round" "-")
((((((triple9) -> (rule4 % int4))) -> (rule1 % int3)) ((triple9) -> (rule2 % int2))) -> (rule6 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int3
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int4
The mouse likes the squirrel.
True
7
proof
[(((((((((triple9) -> rule4)) -> rule1) ((triple9) -> rule2)) -> rule6)) -> rule4))]
("mouse" "likes" "squirrel" "+")
((((((((triple9) -> (rule4 % int5))) -> (rule1 % int4)) ((triple9) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int4
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int5
The mouse does not like the squirrel.
False
7
inv-proof
[(((((((((triple9) -> rule4)) -> rule1) ((triple9) -> rule2)) -> rule6)) -> rule4))]
("mouse" "likes" "squirrel" "-")
((((((((triple9) -> (rule4 % int5))) -> (rule1 % int4)) ((triple9) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int4
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int5
The mouse visits the mouse.
True
8
proof
[(((((((((((triple9) -> rule4)) -> rule1) ((triple9) -> rule2)) -> rule6)) -> rule4)) -> rule1))]
("mouse" "visits" "mouse" "+")
((((((((((triple9) -> (rule4 % int6))) -> (rule1 % int5)) ((triple9) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int5
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int6
The mouse does not visit the mouse.
False
8
inv-proof
[(((((((((((triple9) -> rule4)) -> rule1) ((triple9) -> rule2)) -> rule6)) -> rule4)) -> rule1))]
("mouse" "visits" "mouse" "-")
((((((((((triple9) -> (rule4 % int6))) -> (rule1 % int5)) ((triple9) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int5
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int6
The cat does not visit the mouse.
Unknown
inv-rconc
[@2: The cat visits the mouse.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("cat" "visits" "mouse" "-")
The mouse visits the squirrel.
Unknown
rconc
[@1: The mouse visits the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "visits" "squirrel" "+")
The cat does not like the squirrel.
Unknown
inv-rconc
[@1: The cat likes the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "likes" "squirrel" "-")
The lion likes the squirrel.
Unknown
rconc
[@1: The lion likes the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "likes" "squirrel" "+")
The mouse does not chase the lion.
Unknown
inv-rconc
[@1: The mouse chases the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "chases" "lion" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
The lion does not visit the cat.
Unknown
inv-random
[@0: The lion visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cat" "-")
The squirrel visits the cat.
Unknown
random
[@0: The squirrel visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "cat" "+")
The lion does not visit the squirrel.
Unknown
inv-random
[@0: The lion visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "squirrel" "-")
The lion likes the cat.
Unknown
random
[@0: The lion likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cat" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel chases the mouse.
Unknown
random
[@0: The squirrel chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "mouse" "+")
@0: The cat is not young.[(triple2)] The cat is rough.[(triple1)] The cat visits the squirrel.[(triple3)] The lion chases the mouse.[(triple4)] The lion does not visit the mouse.[(triple5)] The mouse is kind.[(triple6)] The mouse is rough.[(triple7)] The squirrel is kind.[(triple8)] The squirrel is round.[(triple9)] The squirrel is young.[(triple10)] @1: The squirrel is rough.[(((triple9) -> rule2))] The squirrel likes the squirrel.[(((triple9) -> rule4))] @2: The squirrel visits the mouse.[(((((triple9) -> rule4)) -> rule1))] @3: The mouse is round.[(((((((triple9) -> rule4)) -> rule1) ((triple9) -> rule2)) -> rule6))] @4: The mouse likes the squirrel.[(((((((((triple9) -> rule4)) -> rule1) ((triple9) -> rule2)) -> rule6)) -> rule4))] @5: The mouse visits the mouse.[(((((((((((triple9) -> rule4)) -> rule1) ((triple9) -> rule2)) -> rule6)) -> rule4)) -> rule1))]
The cat is not young.
("cat" "is" "young" "-")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple3
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple4
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
triple5
The mouse is kind.
("mouse" "is" "kind" "+")
triple6
The mouse is rough.
("mouse" "is" "rough" "+")
triple7
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple8
The squirrel is round.
("squirrel" "is" "round" "+")
triple9
The squirrel is young.
("squirrel" "is" "young" "+")
triple10
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple9) -> (rule2 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((triple9) -> (rule4 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
((((triple9) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
((((((triple9) -> (rule4 % int4))) -> (rule1 % int3)) ((triple9) -> (rule2 % int2))) -> (rule6 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int3
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int4
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
((((((((triple9) -> (rule4 % int5))) -> (rule1 % int4)) ((triple9) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int4
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int5
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((((((((((triple9) -> (rule4 % int6))) -> (rule1 % int5)) ((triple9) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int5
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int6