The dog chases the squirrel. The dog eats the squirrel. The dog is green. The dog is kind. The dog is rough. The dog sees the squirrel. The squirrel chases the dog. The squirrel is blue. The squirrel is cold. The squirrel is kind. The squirrel is rough. The squirrel sees the dog. If something sees the squirrel then it is kind. If something is rough and it eats the dog then it chases the dog. If something eats the squirrel and the squirrel chases the dog then the dog chases the squirrel. All rough things are cold. If something is green and it sees the dog then the dog is rough. If something chases the squirrel and it is cold then it eats the dog.
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
If something sees the squirrel then it is kind.
((("something" "sees" "squirrel" "+")) -> ("something" "is" "kind" "+"))
If something is rough and it eats the dog then it chases the dog.
((("something" "is" "rough" "+") ("something" "eats" "dog" "+")) -> ("something" "chases" "dog" "+"))
If something eats the squirrel and the squirrel chases the dog then the dog chases the squirrel.
((("something" "eats" "squirrel" "+") ("squirrel" "chases" "dog" "+")) -> ("dog" "chases" "squirrel" "+"))
All rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is green and it sees the dog then the dog is rough.
((("something" "is" "green" "+") ("something" "sees" "dog" "+")) -> ("dog" "is" "rough" "+"))
If something chases the squirrel and it is cold then it eats the dog.
((("something" "chases" "squirrel" "+") ("something" "is" "cold" "+")) -> ("something" "eats" "dog" "+"))
The squirrel chases the dog.
True
1
proof
[(triple7)]
("squirrel" "chases" "dog" "+")
triple7
The dog is not rough.
False
1
inv-proof
[(triple5)]
("dog" "is" "rough" "-")
triple5
The dog is cold.
True
2
proof
[(((triple5) -> rule4))]
("dog" "is" "cold" "+")
((triple5) -> (rule4 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is not cold.
False
2
inv-proof
[(((triple5) -> rule4))]
("dog" "is" "cold" "-")
((triple5) -> (rule4 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog eats the dog.
True
4
proof
[(((triple1 ((triple5) -> rule4)) -> rule6) OR ((((triple2 triple7) -> rule3) ((triple5) -> rule4)) -> rule6))]
("dog" "eats" "dog" "+")
((triple1 ((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
((((triple2 triple7) -> (rule3 % int3)) ((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int3
The dog does not eat the dog.
False
4
inv-proof
[(((triple1 ((triple5) -> rule4)) -> rule6) OR ((((triple2 triple7) -> rule3) ((triple5) -> rule4)) -> rule6))]
("dog" "eats" "dog" "-")
((triple1 ((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
((((triple2 triple7) -> (rule3 % int3)) ((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int3
The dog chases the dog.
True
6
proof
[(((triple5 ((triple1 ((triple5) -> rule4)) -> rule6)) -> rule2) OR ((triple5 ((((triple2 triple7) -> rule3) ((triple5) -> rule4)) -> rule6)) -> rule2))]
("dog" "chases" "dog" "+")
((triple5 ((triple1 ((triple5) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
((triple5 ((((triple2 triple7) -> (rule3 % int4)) ((triple5) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int4
The dog does not chase the dog.
False
6
inv-proof
[(((triple5 ((triple1 ((triple5) -> rule4)) -> rule6)) -> rule2) OR ((triple5 ((((triple2 triple7) -> rule3) ((triple5) -> rule4)) -> rule6)) -> rule2))]
("dog" "chases" "dog" "-")
((triple5 ((triple1 ((triple5) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
((triple5 ((((triple2 triple7) -> (rule3 % int4)) ((triple5) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int4
The squirrel does not eat the dog.
Unknown
inv-rconc
[@1: The squirrel eats the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "eats" "dog" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
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 is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
@0: The dog chases the squirrel.[(triple1 OR ((triple2 triple7) -> rule3))] The dog eats the squirrel.[(triple2)] The dog is green.[(triple3)] The dog is kind.[(triple4 OR ((triple6) -> rule1))] The dog is rough.[(triple5)] The dog sees the squirrel.[(triple6)] The squirrel chases the dog.[(triple7)] The squirrel is blue.[(triple8)] The squirrel is cold.[(triple9 OR ((triple11) -> rule4))] The squirrel is kind.[(triple10)] The squirrel is rough.[(triple11)] The squirrel sees the dog.[(triple12)] @1: The dog is cold.[(((triple5) -> rule4))] @2: The dog eats the dog.[(((triple1 ((triple5) -> rule4)) -> rule6) OR ((((triple2 triple7) -> rule3) ((triple5) -> rule4)) -> rule6))] @3: The dog chases the dog.[(((triple5 ((triple1 ((triple5) -> rule4)) -> rule6)) -> rule2) OR ((triple5 ((((triple2 triple7) -> rule3) ((triple5) -> rule4)) -> rule6)) -> rule2))]
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple1
((triple2 triple7) -> (rule3 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple2
The dog is green.
("dog" "is" "green" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
((triple6) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
triple5
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple6
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple7
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple8
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
((triple11) -> (rule4 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple10
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple11
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple12
The dog is cold.
("dog" "is" "cold" "+")
((triple5) -> (rule4 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
((triple1 ((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
((((triple2 triple7) -> (rule3 % int3)) ((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int3
The dog chases the dog.
("dog" "chases" "dog" "+")
((triple5 ((triple1 ((triple5) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
((triple5 ((((triple2 triple7) -> (rule3 % int4)) ((triple5) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int4