The lion is nice. The lion is round. The lion likes the tiger. The lion needs the tiger. The tiger is big. The tiger is blue. The tiger is round. The tiger likes the lion. The tiger needs the lion. The tiger sees the lion. If someone is red and round then they see the tiger. If someone is round then they see the tiger. If someone needs the lion then the lion is red. If the lion is round then the lion is big. If someone is red then they like the lion. All round people are blue. If the tiger does not need the lion and the lion is not blue then the lion sees the tiger. If someone needs the tiger and the tiger does not like the lion then the tiger is nice.
The lion is nice.
("lion" "is" "nice" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone is red and round then they see the tiger.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "sees" "tiger" "+"))
If someone is round then they see the tiger.
((("someone" "is" "round" "+")) -> ("someone" "sees" "tiger" "+"))
If someone needs the lion then the lion is red.
((("someone" "needs" "lion" "+")) -> ("lion" "is" "red" "+"))
If the lion is round then the lion is big.
((("lion" "is" "round" "+")) -> ("lion" "is" "big" "+"))
If someone is red then they like the lion.
((("someone" "is" "red" "+")) -> ("someone" "likes" "lion" "+"))
All round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If the tiger does not need the lion and the lion is not blue then the lion sees the tiger.
((("tiger" "needs" "lion" "~") ("lion" "is" "blue" "~")) -> ("lion" "sees" "tiger" "+"))
If someone needs the tiger and the tiger does not like the lion then the tiger is nice.
((("someone" "needs" "tiger" "+") ("tiger" "likes" "lion" "~")) -> ("tiger" "is" "nice" "+"))
The lion needs the tiger.
True
1
proof
[(triple4)]
("lion" "needs" "tiger" "+")
triple4
The tiger is not blue.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule6))]
("tiger" "is" "blue" "-")
triple6
((triple7) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger sees the tiger.
True
2
proof
[(((triple7) -> rule2))]
("tiger" "sees" "tiger" "+")
((triple7) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger does not see the tiger.
False
2
inv-proof
[(((triple7) -> rule2))]
("tiger" "sees" "tiger" "-")
((triple7) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The lion likes the lion.
True
3
proof
[(((((triple9) -> rule3)) -> rule5))]
("lion" "likes" "lion" "+")
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion does not like the lion.
False
3
inv-proof
[(((((triple9) -> rule3)) -> rule5))]
("lion" "likes" "lion" "-")
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The tiger is not nice.
Unknown
inv-rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "is" "nice" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The lion is nice.[(triple1)] The lion is round.[(triple2)] The lion likes the tiger.[(triple3)] The lion needs the tiger.[(triple4)] The tiger is big.[(triple5)] The tiger is blue.[(triple6 OR ((triple7) -> rule6))] The tiger is round.[(triple7)] The tiger likes the lion.[(triple8)] The tiger needs the lion.[(triple9)] The tiger sees the lion.[(triple10)] @1: The lion is big.[(((triple2) -> rule4))] The lion is blue.[(((triple2) -> rule6))] The lion is red.[(((triple9) -> rule3))] The lion sees the tiger.[(((triple2) -> rule2) OR ((((triple9) -> rule3) triple2) -> rule1))] The tiger sees the tiger.[(((triple7) -> rule2))] @2: The lion likes the lion.[(((((triple9) -> rule3)) -> rule5))]
The lion is nice.
("lion" "is" "nice" "+")
triple1
The lion is round.
("lion" "is" "round" "+")
triple2
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple3
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple4
The tiger is big.
("tiger" "is" "big" "+")
triple5
The tiger is blue.
("tiger" "is" "blue" "+")
triple6
((triple7) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
triple7
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple8
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple9
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple10
The lion is big.
("lion" "is" "big" "+")
((triple2) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
((triple2) -> (rule6 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is red.
("lion" "is" "red" "+")
((triple9) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((triple2) -> (rule2 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
((((triple9) -> (rule3 % int2)) triple2) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple7) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2