The dog is big. The dog is kind. The dog is round. The dog needs the rabbit. The dog sees the rabbit. The dog visits the rabbit. The rabbit is big. The rabbit is green. The rabbit is red. The rabbit needs the dog. The rabbit does not see the dog. The rabbit visits the dog. If someone is big then they visit the rabbit.
The dog is big.
("dog" "is" "big" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If someone is big then they visit the rabbit.
((("someone" "is" "big" "+")) -> ("someone" "visits" "rabbit" "+"))
The rabbit does not see the dog.
True
1
proof
[(triple11)]
("rabbit" "sees" "dog" "-")
triple11
The dog is not round.
False
1
inv-proof
[(triple3)]
("dog" "is" "round" "-")
triple3
The rabbit visits the rabbit.
True
2
proof
[(((triple7) -> rule1))]
("rabbit" "visits" "rabbit" "+")
((triple7) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit does not visit the rabbit.
False
2
inv-proof
[(((triple7) -> rule1))]
("rabbit" "visits" "rabbit" "-")
((triple7) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The dog is big.[(triple1)] The dog is kind.[(triple2)] The dog is round.[(triple3)] The dog needs the rabbit.[(triple4)] The dog sees the rabbit.[(triple5)] The dog visits the rabbit.[(triple6 OR ((triple1) -> rule1))] The rabbit does not see the dog.[(triple11)] The rabbit is big.[(triple7)] The rabbit is green.[(triple8)] The rabbit is red.[(triple9)] The rabbit needs the dog.[(triple10)] The rabbit visits the dog.[(triple12)] @1: The rabbit visits the rabbit.[(((triple7) -> rule1))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
triple2
The dog is round.
("dog" "is" "round" "+")
triple3
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple4
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple5
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple6
((triple1) -> (rule1 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
triple11
The rabbit is big.
("rabbit" "is" "big" "+")
triple7
The rabbit is green.
("rabbit" "is" "green" "+")
triple8
The rabbit is red.
("rabbit" "is" "red" "+")
triple9
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple10
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple12
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple7) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1