The rabbit is blue. The rabbit is red. The rabbit is young. The rabbit likes the tiger. The rabbit needs the tiger. The rabbit sees the tiger. The tiger is blue. The tiger is nice. The tiger is round. The tiger likes the rabbit. The tiger needs the rabbit. The tiger sees the rabbit. If something sees the rabbit then it likes the rabbit. If something needs the tiger then it is blue. If something is blue then it sees the rabbit.
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something sees the rabbit then it likes the rabbit.
((("something" "sees" "rabbit" "+")) -> ("something" "likes" "rabbit" "+"))
If something needs the tiger then it is blue.
((("something" "needs" "tiger" "+")) -> ("something" "is" "blue" "+"))
If something is blue then it sees the rabbit.
((("something" "is" "blue" "+")) -> ("something" "sees" "rabbit" "+"))
The tiger needs the rabbit.
True
1
proof
[(triple11)]
("tiger" "needs" "rabbit" "+")
triple11
The rabbit is not young.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "young" "-")
triple3
The rabbit sees the rabbit.
True
2
proof
[(((triple1) -> rule3) OR ((((triple5) -> rule2)) -> rule3))]
("rabbit" "sees" "rabbit" "+")
((triple1) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit does not see the rabbit.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((triple5) -> rule2)) -> rule3))]
("rabbit" "sees" "rabbit" "-")
((triple1) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit likes the rabbit.
True
3
proof
[(((((triple1) -> rule3)) -> rule1) OR ((((((triple5) -> rule2)) -> rule3)) -> rule1))]
("rabbit" "likes" "rabbit" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
((((((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The rabbit does not like the rabbit.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1) OR ((((((triple5) -> rule2)) -> rule3)) -> rule1))]
("rabbit" "likes" "rabbit" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
((((((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
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 tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The rabbit is blue.[(triple1 OR ((triple5) -> rule2))] The rabbit is red.[(triple2)] The rabbit is young.[(triple3)] The rabbit likes the tiger.[(triple4)] The rabbit needs the tiger.[(triple5)] The rabbit sees the tiger.[(triple6)] The tiger is blue.[(triple7)] The tiger is nice.[(triple8)] The tiger is round.[(triple9)] The tiger likes the rabbit.[(triple10 OR ((triple12) -> rule1) OR ((((triple7) -> rule3)) -> rule1))] The tiger needs the rabbit.[(triple11)] The tiger sees the rabbit.[(triple12 OR ((triple7) -> rule3))] @1: The rabbit sees the rabbit.[(((triple1) -> rule3) OR ((((triple5) -> rule2)) -> rule3))] @2: The rabbit likes the rabbit.[(((((triple1) -> rule3)) -> rule1) OR ((((((triple5) -> rule2)) -> rule3)) -> rule1))]
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple1
((triple5) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
triple2
The rabbit is young.
("rabbit" "is" "young" "+")
triple3
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple4
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple5
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple6
The tiger is blue.
("tiger" "is" "blue" "+")
triple7
The tiger is nice.
("tiger" "is" "nice" "+")
triple8
The tiger is round.
("tiger" "is" "round" "+")
triple9
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple10
((triple12) -> (rule1 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple11
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple12
((triple7) -> (rule3 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple1) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
((((((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3