The bear visits the squirrel. The squirrel is red. The tiger visits the squirrel. If something is blue then it eats the squirrel. If the tiger is big then the tiger chases the bear. If something visits the tiger then the tiger chases the bear. If something eats the bear then it visits the tiger. If something is blue then it eats the tiger. If something is red then it eats the bear.
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If something is blue then it eats the squirrel.
((("something" "is" "blue" "+")) -> ("something" "eats" "squirrel" "+"))
If the tiger is big then the tiger chases the bear.
((("tiger" "is" "big" "+")) -> ("tiger" "chases" "bear" "+"))
If something visits the tiger then the tiger chases the bear.
((("something" "visits" "tiger" "+")) -> ("tiger" "chases" "bear" "+"))
If something eats the bear then it visits the tiger.
((("something" "eats" "bear" "+")) -> ("something" "visits" "tiger" "+"))
If something is blue then it eats the tiger.
((("something" "is" "blue" "+")) -> ("something" "eats" "tiger" "+"))
If something is red then it eats the bear.
((("something" "is" "red" "+")) -> ("something" "eats" "bear" "+"))
The squirrel is red.
True
1
proof
[(triple2)]
("squirrel" "is" "red" "+")
triple2
The bear does not visit the squirrel.
False
1
inv-proof
[(triple1)]
("bear" "visits" "squirrel" "-")
triple1
The squirrel eats the bear.
True
2
proof
[(((triple2) -> rule6))]
("squirrel" "eats" "bear" "+")
((triple2) -> (rule6 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
The squirrel does not eat the bear.
False
2
inv-proof
[(((triple2) -> rule6))]
("squirrel" "eats" "bear" "-")
((triple2) -> (rule6 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
The squirrel visits the tiger.
True
3
proof
[(((((triple2) -> rule6)) -> rule4))]
("squirrel" "visits" "tiger" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
The squirrel does not visit the tiger.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule4))]
("squirrel" "visits" "tiger" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
The tiger chases the bear.
True
4
proof
[(((((((triple2) -> rule6)) -> rule4)) -> rule3))]
("tiger" "chases" "bear" "+")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int3
The tiger does not chase the bear.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule4)) -> rule3))]
("tiger" "chases" "bear" "-")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int3
The tiger does not visit the tiger.
Unknown
inv-rconc
[@2: The tiger visits the tiger.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger eats the squirrel.
Unknown
rconc
[@1: The tiger eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "eats" "squirrel" "+")
The bear does not visit the tiger.
Unknown
inv-rconc
[@2: The bear visits the tiger.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("bear" "visits" "tiger" "-")
The bear eats the squirrel.
Unknown
rconc
[@1: The bear eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "eats" "squirrel" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The squirrel chases the bear.
Unknown
random
[@0: The squirrel chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "bear" "+")
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 bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
@0: The bear visits the squirrel.[(triple1)] The squirrel is red.[(triple2)] The tiger visits the squirrel.[(triple3)] @1: The squirrel eats the bear.[(((triple2) -> rule6))] @2: The squirrel visits the tiger.[(((((triple2) -> rule6)) -> rule4))] @3: The tiger chases the bear.[(((((((triple2) -> rule6)) -> rule4)) -> rule3))]
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple1
The squirrel is red.
("squirrel" "is" "red" "+")
triple2
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple3
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
((triple2) -> (rule6 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
The tiger chases the bear.
("tiger" "chases" "bear" "+")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int3