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