The cow chases the dog. The cow is round. The cow visits the lion. The dog sees the cow. The dog visits the cow. The lion chases the dog. The lion chases the squirrel. The lion sees the cow. The lion sees the dog. The lion visits the dog. The squirrel is cold. The squirrel visits the cow. If someone chases the squirrel and they are round then they see the squirrel. If someone visits the cow then they visit the dog. If someone sees the cow then they are young. If someone visits the squirrel and they are cold then they visit the cow. If someone is round and cold then they chase the squirrel. If someone is round then they see the dog. If someone chases the dog then they are cold. If someone sees the cow and the cow is cold then the cow chases the squirrel.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow is round.
("cow" "is" "round" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If someone chases the squirrel and they are round then they see the squirrel.
((("someone" "chases" "squirrel" "+") ("someone" "is" "round" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone visits the cow then they visit the dog.
((("someone" "visits" "cow" "+")) -> ("someone" "visits" "dog" "+"))
If someone sees the cow then they are young.
((("someone" "sees" "cow" "+")) -> ("someone" "is" "young" "+"))
If someone visits the squirrel and they are cold then they visit the cow.
((("someone" "visits" "squirrel" "+") ("someone" "is" "cold" "+")) -> ("someone" "visits" "cow" "+"))
If someone is round and cold then they chase the squirrel.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone is round then they see the dog.
((("someone" "is" "round" "+")) -> ("someone" "sees" "dog" "+"))
If someone chases the dog then they are cold.
((("someone" "chases" "dog" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the cow and the cow is cold then the cow chases the squirrel.
((("someone" "sees" "cow" "+") ("cow" "is" "cold" "+")) -> ("cow" "chases" "squirrel" "+"))
The cow chases the dog.
True
1
proof
[(triple1)]
("cow" "chases" "dog" "+")
triple1
The cow does not visit the lion.
False
1
inv-proof
[(triple3)]
("cow" "visits" "lion" "-")
triple3
The squirrel visits the dog.
True
2
proof
[(((triple12) -> rule2))]
("squirrel" "visits" "dog" "+")
((triple12) -> (rule2 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The cow does not see the dog.
False
2
inv-proof
[(((triple2) -> rule6))]
("cow" "sees" "dog" "-")
((triple2) -> (rule6 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow chases the squirrel.
True
4
proof
[(((triple2 ((triple1) -> rule7)) -> rule5) OR ((triple4 ((triple1) -> rule7)) -> rule8) OR ((triple8 ((triple1) -> rule7)) -> rule8))]
("cow" "chases" "squirrel" "+")
((triple2 ((triple1) -> (rule7 % int2))) -> (rule5 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((triple4 ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((triple8 ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow does not chase the squirrel.
False
4
inv-proof
[(((triple2 ((triple1) -> rule7)) -> rule5) OR ((triple4 ((triple1) -> rule7)) -> rule8) OR ((triple8 ((triple1) -> rule7)) -> rule8))]
("cow" "chases" "squirrel" "-")
((triple2 ((triple1) -> (rule7 % int2))) -> (rule5 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((triple4 ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((triple8 ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow sees the squirrel.
True
6
proof
[(((((triple2 ((triple1) -> rule7)) -> rule5) triple2) -> rule1) OR ((((triple4 ((triple1) -> rule7)) -> rule8) triple2) -> rule1) OR ((((triple8 ((triple1) -> rule7)) -> rule8) triple2) -> rule1))]
("cow" "sees" "squirrel" "+")
((((triple2 ((triple1) -> (rule7 % int3))) -> (rule5 % int2)) triple2) -> (rule1 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((triple4 ((triple1) -> (rule7 % int3))) -> (rule8 % int2)) triple2) -> (rule1 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((triple8 ((triple1) -> (rule7 % int3))) -> (rule8 % int2)) triple2) -> (rule1 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow does not see the squirrel.
False
6
inv-proof
[(((((triple2 ((triple1) -> rule7)) -> rule5) triple2) -> rule1) OR ((((triple4 ((triple1) -> rule7)) -> rule8) triple2) -> rule1) OR ((((triple8 ((triple1) -> rule7)) -> rule8) triple2) -> rule1))]
("cow" "sees" "squirrel" "-")
((((triple2 ((triple1) -> (rule7 % int3))) -> (rule5 % int2)) triple2) -> (rule1 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((triple4 ((triple1) -> (rule7 % int3))) -> (rule8 % int2)) triple2) -> (rule1 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((triple8 ((triple1) -> (rule7 % int3))) -> (rule8 % int2)) triple2) -> (rule1 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "young" "-")
The dog chases the squirrel.
Unknown
rconc
[@1: The dog chases the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "chases" "squirrel" "+")
The squirrel does not chase the squirrel.
Unknown
inv-rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "chases" "squirrel" "-")
The dog sees the dog.
Unknown
rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "sees" "dog" "+")
The dog does not chase the cow.
Unknown
inv-random
[@0: The dog chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "cow" "-")
The squirrel visits the lion.
Unknown
random
[@0: The squirrel visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "lion" "+")
The cow does not see the lion.
Unknown
inv-random
[@0: The cow sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "lion" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The cow chases the dog.[(triple1)] The cow is round.[(triple2)] The cow visits the lion.[(triple3)] The dog sees the cow.[(triple4)] The dog visits the cow.[(triple5)] The lion chases the dog.[(triple6)] The lion chases the squirrel.[(triple7)] The lion sees the cow.[(triple8)] The lion sees the dog.[(triple9)] The lion visits the dog.[(triple10)] The squirrel is cold.[(triple11)] The squirrel visits the cow.[(triple12)] @1: The cow is cold.[(((triple1) -> rule7))] The cow sees the dog.[(((triple2) -> rule6))] The dog is young.[(((triple4) -> rule3))] The dog visits the dog.[(((triple5) -> rule2))] The lion is cold.[(((triple6) -> rule7))] The lion is young.[(((triple8) -> rule3))] The squirrel visits the dog.[(((triple12) -> rule2))] @2: The cow chases the squirrel.[(((triple2 ((triple1) -> rule7)) -> rule5) OR ((triple4 ((triple1) -> rule7)) -> rule8) OR ((triple8 ((triple1) -> rule7)) -> rule8))] @3: The cow sees the squirrel.[(((((triple2 ((triple1) -> rule7)) -> rule5) triple2) -> rule1) OR ((((triple4 ((triple1) -> rule7)) -> rule8) triple2) -> rule1) OR ((((triple8 ((triple1) -> rule7)) -> rule8) triple2) -> rule1))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The cow is round.
("cow" "is" "round" "+")
triple2
The cow visits the lion.
("cow" "visits" "lion" "+")
triple3
The dog sees the cow.
("dog" "sees" "cow" "+")
triple4
The dog visits the cow.
("dog" "visits" "cow" "+")
triple5
The lion chases the dog.
("lion" "chases" "dog" "+")
triple6
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple7
The lion sees the cow.
("lion" "sees" "cow" "+")
triple8
The lion sees the dog.
("lion" "sees" "dog" "+")
triple9
The lion visits the dog.
("lion" "visits" "dog" "+")
triple10
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple11
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple12
The cow is cold.
("cow" "is" "cold" "+")
((triple1) -> (rule7 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
((triple2) -> (rule6 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((triple4) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple5) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
((triple6) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is young.
("lion" "is" "young" "+")
((triple8) -> (rule3 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
((triple12) -> (rule2 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
((triple2 ((triple1) -> (rule7 % int2))) -> (rule5 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((triple4 ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((triple8 ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
((((triple2 ((triple1) -> (rule7 % int3))) -> (rule5 % int2)) triple2) -> (rule1 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((triple4 ((triple1) -> (rule7 % int3))) -> (rule8 % int2)) triple2) -> (rule1 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((triple8 ((triple1) -> (rule7 % int3))) -> (rule8 % int2)) triple2) -> (rule1 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3