The lion is big. The lion is red. The lion is rough. The lion is young. The lion needs the rabbit. The lion sees the rabbit. The lion visits the rabbit. The rabbit is big. The rabbit is blue. The rabbit is red. The rabbit is rough. The rabbit is young. The rabbit needs the lion. The rabbit sees the lion. The rabbit visits the lion. If something sees the rabbit and it is blue then it needs the lion. If the rabbit needs the lion and the lion sees the rabbit then the lion is blue. If something sees the rabbit then it sees the lion.
The lion is big.
("lion" "is" "big" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If something sees the rabbit and it is blue then it needs the lion.
((("something" "sees" "rabbit" "+") ("something" "is" "blue" "+")) -> ("something" "needs" "lion" "+"))
If the rabbit needs the lion and the lion sees the rabbit then the lion is blue.
((("rabbit" "needs" "lion" "+") ("lion" "sees" "rabbit" "+")) -> ("lion" "is" "blue" "+"))
If something sees the rabbit then it sees the lion.
((("something" "sees" "rabbit" "+")) -> ("something" "sees" "lion" "+"))
The rabbit is young.
True
1
proof
[(triple12)]
("rabbit" "is" "young" "+")
triple12
The rabbit is not big.
False
1
inv-proof
[(triple8)]
("rabbit" "is" "big" "-")
triple8
The lion sees the lion.
True
2
proof
[(((triple6) -> rule3))]
("lion" "sees" "lion" "+")
((triple6) -> (rule3 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion does not see the lion.
False
2
inv-proof
[(((triple6) -> rule3))]
("lion" "sees" "lion" "-")
((triple6) -> (rule3 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion needs the lion.
True
5
proof
[(((triple6 ((triple13 triple6) -> rule2)) -> rule1))]
("lion" "needs" "lion" "+")
((triple6 ((triple13 triple6) -> (rule2 % int2))) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion does not need the lion.
False
5
inv-proof
[(((triple6 ((triple13 triple6) -> rule2)) -> rule1))]
("lion" "needs" "lion" "-")
((triple6 ((triple13 triple6) -> (rule2 % int2))) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The lion is big.[(triple1)] The lion is red.[(triple2)] The lion is rough.[(triple3)] The lion is young.[(triple4)] The lion needs the rabbit.[(triple5)] The lion sees the rabbit.[(triple6)] The lion visits the rabbit.[(triple7)] The rabbit is big.[(triple8)] The rabbit is blue.[(triple9)] The rabbit is red.[(triple10)] The rabbit is rough.[(triple11)] The rabbit is young.[(triple12)] The rabbit needs the lion.[(triple13)] The rabbit sees the lion.[(triple14)] The rabbit visits the lion.[(triple15)] @1: The lion is blue.[(((triple13 triple6) -> rule2))] The lion sees the lion.[(((triple6) -> rule3))] @2: The lion needs the lion.[(((triple6 ((triple13 triple6) -> rule2)) -> rule1))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is red.
("lion" "is" "red" "+")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple3
The lion is young.
("lion" "is" "young" "+")
triple4
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple5
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple6
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple7
The rabbit is big.
("rabbit" "is" "big" "+")
triple8
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit is red.
("rabbit" "is" "red" "+")
triple10
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple11
The rabbit is young.
("rabbit" "is" "young" "+")
triple12
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple13
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple14
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple15
The lion is blue.
("lion" "is" "blue" "+")
((triple13 triple6) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple6) -> (rule3 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple6 ((triple13 triple6) -> (rule2 % int2))) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2