The bear chases the squirrel. The dog chases the squirrel. The squirrel chases the dog. If the squirrel chases the bear and the bear is young then the bear visits the dog. If something is nice and it visits the dog then it chases the dog. If something is blue then it visits the dog. If something visits the dog then the dog is blue. If the squirrel chases the bear then the squirrel visits the dog. If the dog sees the squirrel and the dog chases the squirrel then the squirrel visits the dog. If something chases the dog then the dog sees the squirrel. If the bear visits the squirrel and the squirrel chases the dog then the bear chases the dog.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
If the squirrel chases the bear and the bear is young then the bear visits the dog.
((("squirrel" "chases" "bear" "+") ("bear" "is" "young" "+")) -> ("bear" "visits" "dog" "+"))
If something is nice and it visits the dog then it chases the dog.
((("something" "is" "nice" "+") ("something" "visits" "dog" "+")) -> ("something" "chases" "dog" "+"))
If something is blue then it visits the dog.
((("something" "is" "blue" "+")) -> ("something" "visits" "dog" "+"))
If something visits the dog then the dog is blue.
((("something" "visits" "dog" "+")) -> ("dog" "is" "blue" "+"))
If the squirrel chases the bear then the squirrel visits the dog.
((("squirrel" "chases" "bear" "+")) -> ("squirrel" "visits" "dog" "+"))
If the dog sees the squirrel and the dog chases the squirrel then the squirrel visits the dog.
((("dog" "sees" "squirrel" "+") ("dog" "chases" "squirrel" "+")) -> ("squirrel" "visits" "dog" "+"))
If something chases the dog then the dog sees the squirrel.
((("something" "chases" "dog" "+")) -> ("dog" "sees" "squirrel" "+"))
If the bear visits the squirrel and the squirrel chases the dog then the bear chases the dog.
((("bear" "visits" "squirrel" "+") ("squirrel" "chases" "dog" "+")) -> ("bear" "chases" "dog" "+"))
The squirrel chases the dog.
True
1
proof
[(triple3)]
("squirrel" "chases" "dog" "+")
triple3
The squirrel does not chase the dog.
False
1
inv-proof
[(triple3)]
("squirrel" "chases" "dog" "-")
triple3
The dog sees the squirrel.
True
2
proof
[(((triple3) -> rule7))]
("dog" "sees" "squirrel" "+")
((triple3) -> (rule7 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The dog does not see the squirrel.
False
2
inv-proof
[(((triple3) -> rule7))]
("dog" "sees" "squirrel" "-")
((triple3) -> (rule7 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The squirrel visits the dog.
True
4
proof
[(((((triple3) -> rule7) triple2) -> rule6))]
("squirrel" "visits" "dog" "+")
((((triple3) -> (rule7 % int2)) triple2) -> (rule6 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int2
The squirrel does not visit the dog.
False
4
inv-proof
[(((((triple3) -> rule7) triple2) -> rule6))]
("squirrel" "visits" "dog" "-")
((((triple3) -> (rule7 % int2)) triple2) -> (rule6 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int2
The dog is blue.
True
5
proof
[(((((((triple3) -> rule7) triple2) -> rule6)) -> rule4))]
("dog" "is" "blue" "+")
((((((triple3) -> (rule7 % int3)) triple2) -> (rule6 % int2))) -> (rule4 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int3
The dog is not blue.
False
5
inv-proof
[(((((((triple3) -> rule7) triple2) -> rule6)) -> rule4))]
("dog" "is" "blue" "-")
((((((triple3) -> (rule7 % int3)) triple2) -> (rule6 % int2))) -> (rule4 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int3
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "dog" "-")
The bear visits the dog.
Unknown
rconc
[@1: The bear visits the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "dog" "+")
The bear does not chase the dog.
Unknown
inv-rconc
[@1: The bear chases the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "chases" "dog" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The dog does not chase the bear.
Unknown
inv-random
[@0: The dog chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "bear" "-")
The squirrel sees the dog.
Unknown
random
[@0: The squirrel sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "dog" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
@0: The bear chases the squirrel.[(triple1)] The dog chases the squirrel.[(triple2)] The squirrel chases the dog.[(triple3)] @1: The dog sees the squirrel.[(((triple3) -> rule7))] @2: The squirrel visits the dog.[(((((triple3) -> rule7) triple2) -> rule6))] @3: The dog is blue.[(((((((triple3) -> rule7) triple2) -> rule6)) -> rule4))] @4: The dog visits the dog.[(((((((((triple3) -> rule7) triple2) -> rule6)) -> rule4)) -> rule3))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple2
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple3
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
((triple3) -> (rule7 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
((((triple3) -> (rule7 % int2)) triple2) -> (rule6 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
((((((triple3) -> (rule7 % int3)) triple2) -> (rule6 % int2))) -> (rule4 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int3
The dog visits the dog.
("dog" "visits" "dog" "+")
((((((((triple3) -> (rule7 % int4)) triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int3
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int4