The dog chases the squirrel. The dog is green. The dog is young. The dog visits the rabbit. The lion chases the squirrel. The lion likes the squirrel. The rabbit likes the lion. The squirrel chases the lion. The squirrel is blue. The squirrel is green. If the rabbit is kind then the rabbit chases the dog. If something chases the squirrel then it is kind. If something is green and it chases the rabbit then the rabbit likes the squirrel. If something likes the squirrel then it is blue. Young things are green. If the dog is kind then the dog chases the rabbit. If the squirrel visits the rabbit then the rabbit chases the squirrel. If the rabbit chases the squirrel then the squirrel is kind. If something is blue then it visits the squirrel.
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is young.
("dog" "is" "young" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
If the rabbit is kind then the rabbit chases the dog.
((("rabbit" "is" "kind" "+")) -> ("rabbit" "chases" "dog" "+"))
If something chases the squirrel then it is kind.
((("something" "chases" "squirrel" "+")) -> ("something" "is" "kind" "+"))
If something is green and it chases the rabbit then the rabbit likes the squirrel.
((("something" "is" "green" "+") ("something" "chases" "rabbit" "+")) -> ("rabbit" "likes" "squirrel" "+"))
If something likes the squirrel then it is blue.
((("something" "likes" "squirrel" "+")) -> ("something" "is" "blue" "+"))
Young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If the dog is kind then the dog chases the rabbit.
((("dog" "is" "kind" "+")) -> ("dog" "chases" "rabbit" "+"))
If the squirrel visits the rabbit then the rabbit chases the squirrel.
((("squirrel" "visits" "rabbit" "+")) -> ("rabbit" "chases" "squirrel" "+"))
If the rabbit chases the squirrel then the squirrel is kind.
((("rabbit" "chases" "squirrel" "+")) -> ("squirrel" "is" "kind" "+"))
If something is blue then it visits the squirrel.
((("something" "is" "blue" "+")) -> ("something" "visits" "squirrel" "+"))
The squirrel chases the lion.
True
1
proof
[(triple8)]
("squirrel" "chases" "lion" "+")
triple8
The dog does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("dog" "chases" "squirrel" "-")
triple1
The squirrel visits the squirrel.
True
2
proof
[(((triple9) -> rule9))]
("squirrel" "visits" "squirrel" "+")
((triple9) -> (rule9 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The lion is not blue.
False
2
inv-proof
[(((triple6) -> rule4))]
("lion" "is" "blue" "-")
((triple6) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The dog chases the rabbit.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("dog" "chases" "rabbit" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The lion does not visit the squirrel.
False
3
inv-proof
[(((((triple6) -> rule4)) -> rule9))]
("lion" "visits" "squirrel" "-")
((((triple6) -> (rule4 % int2))) -> (rule9 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The rabbit likes the squirrel.
True
5
proof
[(((triple2 ((((triple1) -> rule2)) -> rule6)) -> rule3) OR ((((triple3) -> rule5) ((((triple1) -> rule2)) -> rule6)) -> rule3))]
("rabbit" "likes" "squirrel" "+")
((triple2 ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
((((triple3) -> (rule5 % int4)) ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The dog is green.
("dog" "is" "green" "+")
int4
The rabbit does not like the squirrel.
False
5
inv-proof
[(((triple2 ((((triple1) -> rule2)) -> rule6)) -> rule3) OR ((((triple3) -> rule5) ((((triple1) -> rule2)) -> rule6)) -> rule3))]
("rabbit" "likes" "squirrel" "-")
((triple2 ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
((((triple3) -> (rule5 % int4)) ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The dog is green.
("dog" "is" "green" "+")
int4
The rabbit is blue.
True
6
proof
[(((((triple2 ((((triple1) -> rule2)) -> rule6)) -> rule3)) -> rule4) OR ((((((triple3) -> rule5) ((((triple1) -> rule2)) -> rule6)) -> rule3)) -> rule4))]
("rabbit" "is" "blue" "+")
((((triple2 ((((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
((((((triple3) -> (rule5 % int5)) ((((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
The dog is green.
("dog" "is" "green" "+")
int5
The rabbit is not blue.
False
6
inv-proof
[(((((triple2 ((((triple1) -> rule2)) -> rule6)) -> rule3)) -> rule4) OR ((((((triple3) -> rule5) ((((triple1) -> rule2)) -> rule6)) -> rule3)) -> rule4))]
("rabbit" "is" "blue" "-")
((((triple2 ((((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
((((((triple3) -> (rule5 % int5)) ((((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
The dog is green.
("dog" "is" "green" "+")
int5
The rabbit visits the squirrel.
True
7
proof
[(((((((triple2 ((((triple1) -> rule2)) -> rule6)) -> rule3)) -> rule4)) -> rule9) OR ((((((((triple3) -> rule5) ((((triple1) -> rule2)) -> rule6)) -> rule3)) -> rule4)) -> rule9))]
("rabbit" "visits" "squirrel" "+")
((((((triple2 ((((triple1) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int3
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int4
The dog is kind.
("dog" "is" "kind" "+")
int5
((((((((triple3) -> (rule5 % int6)) ((((triple1) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int3
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int4
The dog is kind.
("dog" "is" "kind" "+")
int5
The dog is green.
("dog" "is" "green" "+")
int6
The rabbit does not visit the squirrel.
False
7
inv-proof
[(((((((triple2 ((((triple1) -> rule2)) -> rule6)) -> rule3)) -> rule4)) -> rule9) OR ((((((((triple3) -> rule5) ((((triple1) -> rule2)) -> rule6)) -> rule3)) -> rule4)) -> rule9))]
("rabbit" "visits" "squirrel" "-")
((((((triple2 ((((triple1) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int3
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int4
The dog is kind.
("dog" "is" "kind" "+")
int5
((((((((triple3) -> (rule5 % int6)) ((((triple1) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int3
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int4
The dog is kind.
("dog" "is" "kind" "+")
int5
The dog is green.
("dog" "is" "green" "+")
int6
The squirrel is not kind.
Unknown
inv-rconc
[@2: The squirrel is kind.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("squirrel" "is" "kind" "-")
The rabbit chases the dog.
Unknown
rconc
[@3: The rabbit chases the dog.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule7 <- FAIL)]]
("rabbit" "chases" "dog" "+")
The rabbit does not chase the squirrel.
Unknown
inv-rconc
[@1: The rabbit chases the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "chases" "squirrel" "-")
The lion is green.
Unknown
rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "green" "+")
The rabbit is not green.
Unknown
inv-rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "green" "-")
The dog visits the squirrel.
Unknown
rconc
[@2: The dog visits the squirrel.[CWA. Example of deepest failure = (rule9 <- rule4 <- FAIL)]]
("dog" "visits" "squirrel" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The dog likes the lion.
Unknown
random
[@0: The dog likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "lion" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The lion likes the rabbit.
Unknown
random
[@0: The lion likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "rabbit" "+")
@0: The dog chases the squirrel.[(triple1)] The dog is green.[(triple2 OR ((triple3) -> rule5))] The dog is young.[(triple3)] The dog visits the rabbit.[(triple4)] The lion chases the squirrel.[(triple5)] The lion likes the squirrel.[(triple6)] The rabbit likes the lion.[(triple7)] The squirrel chases the lion.[(triple8)] The squirrel is blue.[(triple9)] The squirrel is green.[(triple10)] @1: The dog is kind.[(((triple1) -> rule2))] The lion is blue.[(((triple6) -> rule4))] The lion is kind.[(((triple5) -> rule2))] The squirrel visits the squirrel.[(((triple9) -> rule9))] @2: The dog chases the rabbit.[(((((triple1) -> rule2)) -> rule6))] The lion visits the squirrel.[(((((triple6) -> rule4)) -> rule9))] @3: The rabbit likes the squirrel.[(((triple2 ((((triple1) -> rule2)) -> rule6)) -> rule3) OR ((((triple3) -> rule5) ((((triple1) -> rule2)) -> rule6)) -> rule3))] @4: The rabbit is blue.[(((((triple2 ((((triple1) -> rule2)) -> rule6)) -> rule3)) -> rule4) OR ((((((triple3) -> rule5) ((((triple1) -> rule2)) -> rule6)) -> rule3)) -> rule4))] @5: The rabbit visits the squirrel.[(((((((triple2 ((((triple1) -> rule2)) -> rule6)) -> rule3)) -> rule4)) -> rule9) OR ((((((((triple3) -> rule5) ((((triple1) -> rule2)) -> rule6)) -> rule3)) -> rule4)) -> rule9))]
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
((triple3) -> (rule5 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is young.
("dog" "is" "young" "+")
triple3
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple4
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple5
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple6
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple7
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple8
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple9
The squirrel is green.
("squirrel" "is" "green" "+")
triple10
The dog is kind.
("dog" "is" "kind" "+")
((triple1) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
((triple6) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((triple5) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple9) -> (rule9 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
((((triple6) -> (rule4 % int2))) -> (rule9 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
((triple2 ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
((((triple3) -> (rule5 % int4)) ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The dog is green.
("dog" "is" "green" "+")
int4
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((triple2 ((((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
((((((triple3) -> (rule5 % int5)) ((((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
The dog is green.
("dog" "is" "green" "+")
int5
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
((((((triple2 ((((triple1) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int3
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int4
The dog is kind.
("dog" "is" "kind" "+")
int5
((((((((triple3) -> (rule5 % int6)) ((((triple1) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int3
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int4
The dog is kind.
("dog" "is" "kind" "+")
int5
The dog is green.
("dog" "is" "green" "+")
int6