The bear does not visit the squirrel. The squirrel is rough. The squirrel visits the bear. If the squirrel visits the bear then the squirrel chases the bear. If the squirrel is cold then the squirrel chases the bear. If the bear likes the squirrel and the squirrel chases the bear then the bear does not visit the squirrel. If something likes the bear then it visits the squirrel. If the squirrel likes the bear and the squirrel chases the bear then the squirrel visits the bear. If something chases the squirrel and the squirrel chases the bear then the bear chases the squirrel. If something likes the squirrel then it chases the squirrel. If something chases the bear then it chases the squirrel.
The bear does not visit the squirrel.
("bear" "visits" "squirrel" "-")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
If the squirrel visits the bear then the squirrel chases the bear.
((("squirrel" "visits" "bear" "+")) -> ("squirrel" "chases" "bear" "+"))
If the squirrel is cold then the squirrel chases the bear.
((("squirrel" "is" "cold" "+")) -> ("squirrel" "chases" "bear" "+"))
If the bear likes the squirrel and the squirrel chases the bear then the bear does not visit the squirrel.
((("bear" "likes" "squirrel" "+") ("squirrel" "chases" "bear" "+")) -> ("bear" "visits" "squirrel" "-"))
If something likes the bear then it visits the squirrel.
((("something" "likes" "bear" "+")) -> ("something" "visits" "squirrel" "+"))
If the squirrel likes the bear and the squirrel chases the bear then the squirrel visits the bear.
((("squirrel" "likes" "bear" "+") ("squirrel" "chases" "bear" "+")) -> ("squirrel" "visits" "bear" "+"))
If something chases the squirrel and the squirrel chases the bear then the bear chases the squirrel.
((("something" "chases" "squirrel" "+") ("squirrel" "chases" "bear" "+")) -> ("bear" "chases" "squirrel" "+"))
If something likes the squirrel then it chases the squirrel.
((("something" "likes" "squirrel" "+")) -> ("something" "chases" "squirrel" "+"))
If something chases the bear then it chases the squirrel.
((("something" "chases" "bear" "+")) -> ("something" "chases" "squirrel" "+"))
The squirrel is rough.
True
1
proof
[(triple2)]
("squirrel" "is" "rough" "+")
triple2
The squirrel is not rough.
False
1
inv-proof
[(triple2)]
("squirrel" "is" "rough" "-")
triple2
The squirrel chases the bear.
True
2
proof
[(((triple3) -> rule1))]
("squirrel" "chases" "bear" "+")
((triple3) -> (rule1 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The squirrel does not chase the bear.
False
2
inv-proof
[(((triple3) -> rule1))]
("squirrel" "chases" "bear" "-")
((triple3) -> (rule1 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The squirrel chases the squirrel.
True
3
proof
[(((((triple3) -> rule1)) -> rule8))]
("squirrel" "chases" "squirrel" "+")
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int2
The squirrel does not chase the squirrel.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule8))]
("squirrel" "chases" "squirrel" "-")
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int2
The bear chases the squirrel.
True
6
proof
[(((((((triple3) -> rule1)) -> rule8) ((triple3) -> rule1)) -> rule6))]
("bear" "chases" "squirrel" "+")
((((((triple3) -> (rule1 % int3))) -> (rule8 % int2)) ((triple3) -> (rule1 % int3))) -> (rule6 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int3
The bear does not chase the squirrel.
False
6
inv-proof
[(((((((triple3) -> rule1)) -> rule8) ((triple3) -> rule1)) -> rule6))]
("bear" "chases" "squirrel" "-")
((((((triple3) -> (rule1 % int3))) -> (rule8 % int2)) ((triple3) -> (rule1 % int3))) -> (rule6 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int3
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The squirrel likes the bear.
Unknown
random
[@0: The squirrel likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "bear" "+")
@0: The bear does not visit the squirrel.[(triple1)] The squirrel is rough.[(triple2)] The squirrel visits the bear.[(triple3)] @1: The squirrel chases the bear.[(((triple3) -> rule1))] @2: The squirrel chases the squirrel.[(((((triple3) -> rule1)) -> rule8))] @3: The bear chases the squirrel.[(((((((triple3) -> rule1)) -> rule8) ((triple3) -> rule1)) -> rule6))]
The bear does not visit the squirrel.
("bear" "visits" "squirrel" "-")
triple1
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple2
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple3
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
((triple3) -> (rule1 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int2
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
((((((triple3) -> (rule1 % int3))) -> (rule8 % int2)) ((triple3) -> (rule1 % int3))) -> (rule6 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int3