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