The lion is kind. The lion is red. The lion likes the squirrel. The lion likes the tiger. The lion visits the tiger. The squirrel eats the lion. The squirrel is big. The squirrel is round. The squirrel likes the lion. The tiger eats the lion. The tiger eats the squirrel. The tiger is blue. The tiger is red. The tiger is round. The tiger visits the lion. If someone is kind then they visit the lion. If the squirrel is round and the squirrel visits the lion then the squirrel likes the tiger. All big people are kind. If someone eats the tiger and the tiger likes the squirrel then the squirrel likes the lion. If someone is round then they like the squirrel. If someone is round and red then they like the tiger.
The lion is kind.
("lion" "is" "kind" "+")
The lion is red.
("lion" "is" "red" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone is kind then they visit the lion.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "lion" "+"))
If the squirrel is round and the squirrel visits the lion then the squirrel likes the tiger.
((("squirrel" "is" "round" "+") ("squirrel" "visits" "lion" "+")) -> ("squirrel" "likes" "tiger" "+"))
All big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone eats the tiger and the tiger likes the squirrel then the squirrel likes the lion.
((("someone" "eats" "tiger" "+") ("tiger" "likes" "squirrel" "+")) -> ("squirrel" "likes" "lion" "+"))
If someone is round then they like the squirrel.
((("someone" "is" "round" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone is round and red then they like the tiger.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "likes" "tiger" "+"))
The lion likes the squirrel.
True
1
proof
[(triple3)]
("lion" "likes" "squirrel" "+")
triple3
The lion is not red.
False
1
inv-proof
[(triple2)]
("lion" "is" "red" "-")
triple2
The tiger likes the squirrel.
True
2
proof
[(((triple14) -> rule5))]
("tiger" "likes" "squirrel" "+")
((triple14) -> (rule5 % int1))
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int1
The squirrel does not like the squirrel.
False
2
inv-proof
[(((triple8) -> rule5))]
("squirrel" "likes" "squirrel" "-")
((triple8) -> (rule5 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel visits the lion.
True
3
proof
[(((((triple7) -> rule3)) -> rule1))]
("squirrel" "visits" "lion" "+")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel does not visit the lion.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule1))]
("squirrel" "visits" "lion" "-")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel likes the tiger.
True
5
proof
[(((triple8 ((((triple7) -> rule3)) -> rule1)) -> rule2))]
("squirrel" "likes" "tiger" "+")
((triple8 ((((triple7) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
The squirrel does not like the tiger.
False
5
inv-proof
[(((triple8 ((((triple7) -> rule3)) -> rule1)) -> rule2))]
("squirrel" "likes" "tiger" "-")
((triple8 ((((triple7) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "kind" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The lion does not eat the tiger.
Unknown
inv-random
[@0: The lion eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "tiger" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The squirrel is not red.
Unknown
inv-random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
@0: The lion is kind.[(triple1)] The lion is red.[(triple2)] The lion likes the squirrel.[(triple3)] The lion likes the tiger.[(triple4)] The lion visits the tiger.[(triple5)] The squirrel eats the lion.[(triple6)] The squirrel is big.[(triple7)] The squirrel is round.[(triple8)] The squirrel likes the lion.[(triple9)] The tiger eats the lion.[(triple10)] The tiger eats the squirrel.[(triple11)] The tiger is blue.[(triple12)] The tiger is red.[(triple13)] The tiger is round.[(triple14)] The tiger visits the lion.[(triple15)] @1: The lion visits the lion.[(((triple1) -> rule1))] The squirrel is kind.[(((triple7) -> rule3))] The squirrel likes the squirrel.[(((triple8) -> rule5))] The tiger likes the squirrel.[(((triple14) -> rule5))] The tiger likes the tiger.[(((triple14 triple13) -> rule6))] @2: The squirrel visits the lion.[(((((triple7) -> rule3)) -> rule1))] @3: The squirrel likes the tiger.[(((triple8 ((((triple7) -> rule3)) -> rule1)) -> rule2))]
The lion is kind.
("lion" "is" "kind" "+")
triple1
The lion is red.
("lion" "is" "red" "+")
triple2
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple3
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple4
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple5
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple6
The squirrel is big.
("squirrel" "is" "big" "+")
triple7
The squirrel is round.
("squirrel" "is" "round" "+")
triple8
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple9
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple10
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple11
The tiger is blue.
("tiger" "is" "blue" "+")
triple12
The tiger is red.
("tiger" "is" "red" "+")
triple13
The tiger is round.
("tiger" "is" "round" "+")
triple14
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple15
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple1) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple7) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((triple8) -> (rule5 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
((triple14) -> (rule5 % int1))
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple14 triple13) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
((triple8 ((((triple7) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3