The dog is green. The dog visits the rabbit. The rabbit is not round. The rabbit sees the tiger. The rabbit visits the dog. The rabbit visits the tiger. The tiger is red. If something is red then it does not see the rabbit.
The dog is green.
("dog" "is" "green" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit is not round.
("rabbit" "is" "round" "-")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
If something is red then it does not see the rabbit.
((("something" "is" "red" "+")) -> ("something" "sees" "rabbit" "-"))
The rabbit is not round.
True
1
proof
[(triple3)]
("rabbit" "is" "round" "-")
triple3
The rabbit does not visit the tiger.
False
1
inv-proof
[(triple6)]
("rabbit" "visits" "tiger" "-")
triple6
The tiger does not see the rabbit.
True
2
proof
[(((triple7) -> rule1))]
("tiger" "sees" "rabbit" "-")
((triple7) -> (rule1 % int1))
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
int1
The tiger sees the rabbit.
False
2
inv-proof
[(((triple7) -> rule1))]
("tiger" "sees" "rabbit" "+")
((triple7) -> (rule1 % int1))
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
int1
The dog does not need the rabbit.
Unknown
inv-random
[@0: The dog needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The dog is green.[(triple1)] The dog visits the rabbit.[(triple2)] The rabbit is not round.[(triple3)] The rabbit sees the tiger.[(triple4)] The rabbit visits the dog.[(triple5)] The rabbit visits the tiger.[(triple6)] The tiger is red.[(triple7)] @1: The tiger does not see the rabbit.[(((triple7) -> rule1))]
The dog is green.
("dog" "is" "green" "+")
triple1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple2
The rabbit is not round.
("rabbit" "is" "round" "-")
triple3
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple4
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple5
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple6
The tiger is red.
("tiger" "is" "red" "+")
triple7
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
((triple7) -> (rule1 % int1))
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
int1