The dog chases the squirrel. The dog is cold. The squirrel chases the dog. If something sees the squirrel then it chases the dog. If something chases the squirrel then it is red. If the squirrel likes the dog and the dog likes the squirrel then the squirrel chases the dog. If something likes the dog and the dog is rough then it is cold. If something chases the dog then it likes the squirrel. If something chases the squirrel then it sees the squirrel.
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The dog is cold.
("dog" "is" "cold" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
If something sees the squirrel then it chases the dog.
((("something" "sees" "squirrel" "+")) -> ("something" "chases" "dog" "+"))
If something chases the squirrel then it is red.
((("something" "chases" "squirrel" "+")) -> ("something" "is" "red" "+"))
If the squirrel likes the dog and the dog likes the squirrel then the squirrel chases the dog.
((("squirrel" "likes" "dog" "+") ("dog" "likes" "squirrel" "+")) -> ("squirrel" "chases" "dog" "+"))
If something likes the dog and the dog is rough then it is cold.
((("something" "likes" "dog" "+") ("dog" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something chases the dog then it likes the squirrel.
((("something" "chases" "dog" "+")) -> ("something" "likes" "squirrel" "+"))
If something chases the squirrel then it sees the squirrel.
((("something" "chases" "squirrel" "+")) -> ("something" "sees" "squirrel" "+"))
The dog is cold.
True
1
proof
[(triple2)]
("dog" "is" "cold" "+")
triple2
The squirrel does not chase the dog.
False
1
inv-proof
[(triple3)]
("squirrel" "chases" "dog" "-")
triple3
The dog is red.
True
2
proof
[(((triple1) -> rule2))]
("dog" "is" "red" "+")
((triple1) -> (rule2 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog does not see the squirrel.
False
2
inv-proof
[(((triple1) -> rule6))]
("dog" "sees" "squirrel" "-")
((triple1) -> (rule6 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The dog chases the dog.
True
3
proof
[(((((triple1) -> rule6)) -> rule1))]
("dog" "chases" "dog" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int2
The dog does not chase the dog.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule1))]
("dog" "chases" "dog" "-")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int2
The dog likes the squirrel.
True
4
proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule5))]
("dog" "likes" "squirrel" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int3
The dog does not like the squirrel.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule5))]
("dog" "likes" "squirrel" "-")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int3
The squirrel is not red.
Unknown
inv-rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "red" "-")
The squirrel is cold.
Unknown
rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "cold" "+")
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The dog chases the squirrel.[(triple1)] The dog is cold.[(triple2)] The squirrel chases the dog.[(triple3)] @1: The dog is red.[(((triple1) -> rule2))] The dog sees the squirrel.[(((triple1) -> rule6))] The squirrel likes the squirrel.[(((triple3) -> rule5))] @2: The dog chases the dog.[(((((triple1) -> rule6)) -> rule1))] @3: The dog likes the squirrel.[(((((((triple1) -> rule6)) -> rule1)) -> rule5))]
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
((triple1) -> (rule2 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
((triple1) -> (rule6 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((triple3) -> (rule5 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int2
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int3