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