The dog chases the squirrel. The dog is cold. The squirrel does not see the dog. If someone is big then they do not see the dog. If someone chases the squirrel and the squirrel is not rough then they see the dog. If the dog does not see the squirrel then the squirrel is nice. If someone is nice and they do not see the squirrel then the squirrel does not chase the dog. If the squirrel eats the dog then the dog is big. If someone chases the squirrel then the squirrel eats the dog.
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The dog is cold.
("dog" "is" "cold" "+")
The squirrel does not see the dog.
("squirrel" "sees" "dog" "-")
If someone is big then they do not see the dog.
((("someone" "is" "big" "+")) -> ("someone" "sees" "dog" "-"))
If someone chases the squirrel and the squirrel is not rough then they see the dog.
((("someone" "chases" "squirrel" "+") ("squirrel" "is" "rough" "~")) -> ("someone" "sees" "dog" "+"))
If the dog does not see the squirrel then the squirrel is nice.
((("dog" "sees" "squirrel" "~")) -> ("squirrel" "is" "nice" "+"))
If someone is nice and they do not see the squirrel then the squirrel does not chase the dog.
((("someone" "is" "nice" "+") ("someone" "sees" "squirrel" "~")) -> ("squirrel" "chases" "dog" "-"))
If the squirrel eats the dog then the dog is big.
((("squirrel" "eats" "dog" "+")) -> ("dog" "is" "big" "+"))
If someone chases the squirrel then the squirrel eats the dog.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "eats" "dog" "+"))
The dog chases the squirrel.
True
1
proof
[(triple1)]
("dog" "chases" "squirrel" "+")
triple1
The squirrel sees the dog.
False
1
inv-proof
[(triple3)]
("squirrel" "sees" "dog" "+")
triple3
The squirrel eats the dog.
True
2
proof
[(((triple1) -> rule6))]
("squirrel" "eats" "dog" "+")
((triple1) -> (rule6 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel does not eat the dog.
False
2
inv-proof
[(((triple1) -> rule6))]
("squirrel" "eats" "dog" "-")
((triple1) -> (rule6 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The dog is big.
True
3
proof
[(((((triple1) -> rule6)) -> rule5))]
("dog" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int2
The dog is not big.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule5))]
("dog" "is" "big" "-")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int2
The dog does not see the dog.
True
4
proof
[(((((((triple1) -> rule6)) -> rule5)) -> rule1))]
("dog" "sees" "dog" "-")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog does not see the dog.
("dog" "sees" "dog" "-")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int3
The dog sees the dog.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule5)) -> rule1))]
("dog" "sees" "dog" "+")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog does not see the dog.
("dog" "sees" "dog" "-")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int3
The squirrel is not nice.
Unknown
inv-rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "nice" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The dog does not eat the squirrel.
Unknown
inv-random
[@0: The dog eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "squirrel" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
@0: The dog chases the squirrel.[(triple1)] The dog is cold.[(triple2)] The squirrel does not see the dog.[(triple3)] @1: The squirrel eats the dog.[(((triple1) -> rule6))] @2: The dog is big.[(((((triple1) -> rule6)) -> rule5))] @3: The dog does not see the dog.[(((((((triple1) -> rule6)) -> rule5)) -> rule1))]
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The squirrel does not see the dog.
("squirrel" "sees" "dog" "-")
triple3
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
((triple1) -> (rule6 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The dog is big.
("dog" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int2
The dog does not see the dog.
("dog" "sees" "dog" "-")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog does not see the dog.
("dog" "sees" "dog" "-")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int3