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