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