The dog is big. The dog is green. The dog is kind. The dog is rough. The dog is round. The dog needs the tiger. The dog sees the tiger. The dog visits the tiger. The tiger is big. The tiger is green. The tiger is kind. The tiger is rough. The tiger is round. The tiger needs the dog. The tiger sees the dog. The tiger visits the dog. If something is green and it needs the dog then it visits the tiger. If something sees the tiger and the tiger visits the dog then the tiger needs the dog. If something is round and kind then it visits the tiger. If something visits the tiger then it needs the tiger. If something sees the dog then it visits the tiger. If something is round then it visits the tiger.
The dog is big.
("dog" "is" "big" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something is green and it needs the dog then it visits the tiger.
((("something" "is" "green" "+") ("something" "needs" "dog" "+")) -> ("something" "visits" "tiger" "+"))
If something sees the tiger and the tiger visits the dog then the tiger needs the dog.
((("something" "sees" "tiger" "+") ("tiger" "visits" "dog" "+")) -> ("tiger" "needs" "dog" "+"))
If something is round and kind then it visits the tiger.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "visits" "tiger" "+"))
If something visits the tiger then it needs the tiger.
((("something" "visits" "tiger" "+")) -> ("something" "needs" "tiger" "+"))
If something sees the dog then it visits the tiger.
((("something" "sees" "dog" "+")) -> ("something" "visits" "tiger" "+"))
If something is round then it visits the tiger.
((("something" "is" "round" "+")) -> ("something" "visits" "tiger" "+"))
The dog is rough.
True
1
proof
[(triple4)]
("dog" "is" "rough" "+")
triple4
The dog does not visit the tiger.
False
1
inv-proof
[(triple8 OR ((triple5) -> rule6) OR ((triple5 triple3) -> rule3))]
("dog" "visits" "tiger" "-")
triple8
((triple5) -> (rule6 % int1))
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int1
((triple5 triple3) -> (rule3 % int1))
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int1
The tiger visits the tiger.
True
2
proof
[(((triple13) -> rule6) OR ((triple15) -> rule5) OR ((triple10 triple14) -> rule1) OR ((triple13 triple11) -> rule3) OR ((triple10 ((triple7 triple16) -> rule2)) -> rule1))]
("tiger" "visits" "tiger" "+")
((triple13) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((triple15) -> (rule5 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((triple10 triple14) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((triple13 triple11) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((triple10 ((triple7 triple16) -> (rule2 % int2))) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger does not visit the tiger.
False
2
inv-proof
[(((triple13) -> rule6) OR ((triple15) -> rule5) OR ((triple10 triple14) -> rule1) OR ((triple13 triple11) -> rule3) OR ((triple10 ((triple7 triple16) -> rule2)) -> rule1))]
("tiger" "visits" "tiger" "-")
((triple13) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((triple15) -> (rule5 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((triple10 triple14) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((triple13 triple11) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((triple10 ((triple7 triple16) -> (rule2 % int2))) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger needs the tiger.
True
3
proof
[(((((triple13) -> rule6)) -> rule4) OR ((((triple15) -> rule5)) -> rule4) OR ((((triple10 triple14) -> rule1)) -> rule4) OR ((((triple13 triple11) -> rule3)) -> rule4) OR ((((triple10 ((triple7 triple16) -> rule2)) -> rule1)) -> rule4))]
("tiger" "needs" "tiger" "+")
((((triple13) -> (rule6 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((triple15) -> (rule5 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((triple10 triple14) -> (rule1 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((triple13 triple11) -> (rule3 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((triple10 ((triple7 triple16) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3
The tiger does not need the tiger.
False
3
inv-proof
[(((((triple13) -> rule6)) -> rule4) OR ((((triple15) -> rule5)) -> rule4) OR ((((triple10 triple14) -> rule1)) -> rule4) OR ((((triple13 triple11) -> rule3)) -> rule4) OR ((((triple10 ((triple7 triple16) -> rule2)) -> rule1)) -> rule4))]
("tiger" "needs" "tiger" "-")
((((triple13) -> (rule6 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((triple15) -> (rule5 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((triple10 triple14) -> (rule1 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((triple13 triple11) -> (rule3 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((triple10 ((triple7 triple16) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The dog is big.[(triple1)] The dog is green.[(triple2)] The dog is kind.[(triple3)] The dog is rough.[(triple4)] The dog is round.[(triple5)] The dog needs the tiger.[(triple6 OR ((triple8) -> rule4) OR ((((triple5) -> rule6)) -> rule4) OR ((((triple5 triple3) -> rule3)) -> rule4))] The dog sees the tiger.[(triple7)] The dog visits the tiger.[(triple8 OR ((triple5) -> rule6) OR ((triple5 triple3) -> rule3))] The tiger is big.[(triple9)] The tiger is green.[(triple10)] The tiger is kind.[(triple11)] The tiger is rough.[(triple12)] The tiger is round.[(triple13)] The tiger needs the dog.[(triple14 OR ((triple7 triple16) -> rule2))] The tiger sees the dog.[(triple15)] The tiger visits the dog.[(triple16)] @1: The tiger visits the tiger.[(((triple13) -> rule6) OR ((triple15) -> rule5) OR ((triple10 triple14) -> rule1) OR ((triple13 triple11) -> rule3) OR ((triple10 ((triple7 triple16) -> rule2)) -> rule1))] @2: The tiger needs the tiger.[(((((triple13) -> rule6)) -> rule4) OR ((((triple15) -> rule5)) -> rule4) OR ((((triple10 triple14) -> rule1)) -> rule4) OR ((((triple13 triple11) -> rule3)) -> rule4) OR ((((triple10 ((triple7 triple16) -> rule2)) -> rule1)) -> rule4))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple5
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple6
((triple8) -> (rule4 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int2
((((triple5 triple3) -> (rule3 % int2))) -> (rule4 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int2
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple7
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple8
((triple5) -> (rule6 % int1))
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int1
((triple5 triple3) -> (rule3 % int1))
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is green.
("tiger" "is" "green" "+")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger is round.
("tiger" "is" "round" "+")
triple13
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple14
((triple7 triple16) -> (rule2 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple15
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple16
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple13) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((triple15) -> (rule5 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((triple10 triple14) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((triple13 triple11) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((triple10 ((triple7 triple16) -> (rule2 % int2))) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((triple13) -> (rule6 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((triple15) -> (rule5 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((triple10 triple14) -> (rule1 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((triple13 triple11) -> (rule3 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((triple10 ((triple7 triple16) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3