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