The bear eats the tiger. The squirrel likes the tiger. The tiger is blue. If something likes the tiger and it is nice then the tiger likes the squirrel. If something likes the tiger then it is nice. If something visits the bear and the bear eats the squirrel then the bear visits the squirrel. If something is blue and it likes the squirrel then it is big. If the tiger is big then the tiger visits the squirrel. If something is big and it visits the tiger then the tiger visits the squirrel.
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If something likes the tiger and it is nice then the tiger likes the squirrel.
((("something" "likes" "tiger" "+") ("something" "is" "nice" "+")) -> ("tiger" "likes" "squirrel" "+"))
If something likes the tiger then it is nice.
((("something" "likes" "tiger" "+")) -> ("something" "is" "nice" "+"))
If something visits the bear and the bear eats the squirrel then the bear visits the squirrel.
((("something" "visits" "bear" "+") ("bear" "eats" "squirrel" "+")) -> ("bear" "visits" "squirrel" "+"))
If something is blue and it likes the squirrel then it is big.
((("something" "is" "blue" "+") ("something" "likes" "squirrel" "+")) -> ("something" "is" "big" "+"))
If the tiger is big then the tiger visits the squirrel.
((("tiger" "is" "big" "+")) -> ("tiger" "visits" "squirrel" "+"))
If something is big and it visits the tiger then the tiger visits the squirrel.
((("something" "is" "big" "+") ("something" "visits" "tiger" "+")) -> ("tiger" "visits" "squirrel" "+"))
The bear eats the tiger.
True
1
proof
[(triple1)]
("bear" "eats" "tiger" "+")
triple1
The bear does not eat the tiger.
False
1
inv-proof
[(triple1)]
("bear" "eats" "tiger" "-")
triple1
The squirrel is nice.
True
2
proof
[(((triple2) -> rule2))]
("squirrel" "is" "nice" "+")
((triple2) -> (rule2 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is not nice.
False
2
inv-proof
[(((triple2) -> rule2))]
("squirrel" "is" "nice" "-")
((triple2) -> (rule2 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The tiger likes the squirrel.
True
4
proof
[(((triple2 ((triple2) -> rule2)) -> rule1))]
("tiger" "likes" "squirrel" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The tiger does not like the squirrel.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule1))]
("tiger" "likes" "squirrel" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is not big.
Unknown
inv-rconc
[@1: The squirrel is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "big" "-")
The bear is big.
Unknown
rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "big" "+")
The bear does not visit the squirrel.
Unknown
inv-rconc
[@1: The bear visits the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "visits" "squirrel" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The squirrel does not visit the tiger.
Unknown
inv-random
[@0: The squirrel visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "tiger" "-")
The squirrel eats the bear.
Unknown
random
[@0: The squirrel eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "bear" "+")
@0: The bear eats the tiger.[(triple1)] The squirrel likes the tiger.[(triple2)] The tiger is blue.[(triple3)] @1: The squirrel is nice.[(((triple2) -> rule2))] @2: The tiger likes the squirrel.[(((triple2 ((triple2) -> rule2)) -> rule1))] @3: The tiger is big.[(((triple3 ((triple2 ((triple2) -> rule2)) -> rule1)) -> rule4))] @4: The tiger visits the squirrel.[(((((triple3 ((triple2 ((triple2) -> rule2)) -> rule1)) -> rule4)) -> rule5))]
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple2
The tiger is blue.
("tiger" "is" "blue" "+")
triple3
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple2) -> (rule2 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
((triple3 ((triple2 ((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
((((triple3 ((triple2 ((triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int3
The squirrel is nice.
("squirrel" "is" "nice" "+")
int4