The dog chases the squirrel. The dog eats the squirrel. The dog is nice. The dog is round. The dog sees the squirrel. The squirrel chases the dog. The squirrel eats the dog. The squirrel is blue. The squirrel is cold. The squirrel is nice. The squirrel is round. The squirrel sees the dog. If someone sees the squirrel and the squirrel sees the dog then they chase the dog.
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is round.
("dog" "is" "round" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
If someone sees the squirrel and the squirrel sees the dog then they chase the dog.
((("someone" "sees" "squirrel" "+") ("squirrel" "sees" "dog" "+")) -> ("someone" "chases" "dog" "+"))
The squirrel sees the dog.
True
1
proof
[(triple12)]
("squirrel" "sees" "dog" "+")
triple12
The dog does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("dog" "chases" "squirrel" "-")
triple1
The dog chases the dog.
True
3
proof
[(((triple5 triple12) -> rule1))]
("dog" "chases" "dog" "+")
((triple5 triple12) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog does not chase the dog.
False
3
inv-proof
[(((triple5 triple12) -> rule1))]
("dog" "chases" "dog" "-")
((triple5 triple12) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The dog chases the squirrel.[(triple1)] The dog eats the squirrel.[(triple2)] The dog is nice.[(triple3)] The dog is round.[(triple4)] The dog sees the squirrel.[(triple5)] The squirrel chases the dog.[(triple6)] The squirrel eats the dog.[(triple7)] The squirrel is blue.[(triple8)] The squirrel is cold.[(triple9)] The squirrel is nice.[(triple10)] The squirrel is round.[(triple11)] The squirrel sees the dog.[(triple12)] @1: The dog chases the dog.[(((triple5 triple12) -> rule1))]
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple1
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3
The dog is round.
("dog" "is" "round" "+")
triple4
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple5
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple6
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple7
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple8
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple10
The squirrel is round.
("squirrel" "is" "round" "+")
triple11
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple12
The dog chases the dog.
("dog" "chases" "dog" "+")
((triple5 triple12) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1