The dog is cold. The dog needs the squirrel. The squirrel is young. If someone is round then they need the dog. If someone needs the squirrel and they see the dog then the squirrel sees the dog. If someone visits the dog then the dog is cold. If someone needs the squirrel then they visit the squirrel. If someone visits the squirrel then the squirrel sees the dog. If someone sees the dog then they need the dog.
The dog is cold.
("dog" "is" "cold" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
If someone is round then they need the dog.
((("someone" "is" "round" "+")) -> ("someone" "needs" "dog" "+"))
If someone needs the squirrel and they see the dog then the squirrel sees the dog.
((("someone" "needs" "squirrel" "+") ("someone" "sees" "dog" "+")) -> ("squirrel" "sees" "dog" "+"))
If someone visits the dog then the dog is cold.
((("someone" "visits" "dog" "+")) -> ("dog" "is" "cold" "+"))
If someone needs the squirrel then they visit the squirrel.
((("someone" "needs" "squirrel" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone visits the squirrel then the squirrel sees the dog.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "sees" "dog" "+"))
If someone sees the dog then they need the dog.
((("someone" "sees" "dog" "+")) -> ("someone" "needs" "dog" "+"))
The squirrel is young.
True
1
proof
[(triple3)]
("squirrel" "is" "young" "+")
triple3
The squirrel is not young.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "young" "-")
triple3
The dog visits the squirrel.
True
2
proof
[(((triple2) -> rule4))]
("dog" "visits" "squirrel" "+")
((triple2) -> (rule4 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The dog does not visit the squirrel.
False
2
inv-proof
[(((triple2) -> rule4))]
("dog" "visits" "squirrel" "-")
((triple2) -> (rule4 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The squirrel sees the dog.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("squirrel" "sees" "dog" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
The squirrel does not see the dog.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("squirrel" "sees" "dog" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
The squirrel needs the dog.
True
4
proof
[(((((((triple2) -> rule4)) -> rule5)) -> rule6))]
("squirrel" "needs" "dog" "+")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int3
The squirrel does not need the dog.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule5)) -> rule6))]
("squirrel" "needs" "dog" "-")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int3
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The dog needs the dog.
Unknown
rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "needs" "dog" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel does not visit the dog.
Unknown
inv-random
[@0: The squirrel visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "dog" "-")
The dog sees the squirrel.
Unknown
random
[@0: The dog sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "squirrel" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
@0: The dog is cold.[(triple1)] The dog needs the squirrel.[(triple2)] The squirrel is young.[(triple3)] @1: The dog visits the squirrel.[(((triple2) -> rule4))] @2: The squirrel sees the dog.[(((((triple2) -> rule4)) -> rule5))] @3: The squirrel needs the dog.[(((((((triple2) -> rule4)) -> rule5)) -> rule6))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple2
The squirrel is young.
("squirrel" "is" "young" "+")
triple3
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
((triple2) -> (rule4 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int3