The bald eagle is round. The bald eagle needs the dog. The bald eagle needs the rabbit. The bald eagle needs the squirrel. The bald eagle visits the dog. The bald eagle visits the rabbit. The dog chases the rabbit. The dog is big. The dog visits the rabbit. The rabbit needs the bald eagle. The rabbit visits the squirrel. The squirrel is big. The squirrel visits the bald eagle. The squirrel visits the rabbit. If something is big then it needs the rabbit. If something needs the rabbit and it visits the bald eagle then it is blue. If something visits the bald eagle and it visits the dog then the dog is blue. If something is blue then it visits the dog. If something is blue then it chases the dog.
The bald eagle is round.
("bald eagle" "is" "round" "+")
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
The bald eagle needs the squirrel.
("bald eagle" "needs" "squirrel" "+")
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog is big.
("dog" "is" "big" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If something is big then it needs the rabbit.
((("something" "is" "big" "+")) -> ("something" "needs" "rabbit" "+"))
If something needs the rabbit and it visits the bald eagle then it is blue.
((("something" "needs" "rabbit" "+") ("something" "visits" "bald eagle" "+")) -> ("something" "is" "blue" "+"))
If something visits the bald eagle and it visits the dog then the dog is blue.
((("something" "visits" "bald eagle" "+") ("something" "visits" "dog" "+")) -> ("dog" "is" "blue" "+"))
If something is blue then it visits the dog.
((("something" "is" "blue" "+")) -> ("something" "visits" "dog" "+"))
If something is blue then it chases the dog.
((("something" "is" "blue" "+")) -> ("something" "chases" "dog" "+"))
The squirrel is big.
True
1
proof
[(triple12)]
("squirrel" "is" "big" "+")
triple12
The bald eagle does not need the rabbit.
False
1
inv-proof
[(triple3)]
("bald eagle" "needs" "rabbit" "-")
triple3
The dog needs the rabbit.
True
2
proof
[(((triple8) -> rule1))]
("dog" "needs" "rabbit" "+")
((triple8) -> (rule1 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The dog does not need the rabbit.
False
2
inv-proof
[(((triple8) -> rule1))]
("dog" "needs" "rabbit" "-")
((triple8) -> (rule1 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The squirrel is blue.
True
4
proof
[(((((triple12) -> rule1) triple13) -> rule2))]
("squirrel" "is" "blue" "+")
((((triple12) -> (rule1 % int2)) triple13) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int2
The squirrel is not blue.
False
4
inv-proof
[(((((triple12) -> rule1) triple13) -> rule2))]
("squirrel" "is" "blue" "-")
((((triple12) -> (rule1 % int2)) triple13) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int2
The squirrel chases the dog.
True
5
proof
[(((((((triple12) -> rule1) triple13) -> rule2)) -> rule5))]
("squirrel" "chases" "dog" "+")
((((((triple12) -> (rule1 % int3)) triple13) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int3
The squirrel does not chase the dog.
False
5
inv-proof
[(((((((triple12) -> rule1) triple13) -> rule2)) -> rule5))]
("squirrel" "chases" "dog" "-")
((((((triple12) -> (rule1 % int3)) triple13) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int3
The dog is blue.
True
7
proof
[(((triple13 ((((((triple12) -> rule1) triple13) -> rule2)) -> rule4)) -> rule3))]
("dog" "is" "blue" "+")
((triple13 ((((((triple12) -> (rule1 % int4)) triple13) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int4
The dog is not blue.
False
7
inv-proof
[(((triple13 ((((((triple12) -> rule1) triple13) -> rule2)) -> rule4)) -> rule3))]
("dog" "is" "blue" "-")
((triple13 ((((((triple12) -> (rule1 % int4)) triple13) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int4
The dog visits the dog.
True
8
proof
[(((((triple13 ((((((triple12) -> rule1) triple13) -> rule2)) -> rule4)) -> rule3)) -> rule4))]
("dog" "visits" "dog" "+")
((((triple13 ((((((triple12) -> (rule1 % int5)) triple13) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule4 % 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 squirrel is blue.
("squirrel" "is" "blue" "+")
int4
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int5
The dog does not visit the dog.
False
8
inv-proof
[(((((triple13 ((((((triple12) -> rule1) triple13) -> rule2)) -> rule4)) -> rule3)) -> rule4))]
("dog" "visits" "dog" "-")
((((triple13 ((((((triple12) -> (rule1 % int5)) triple13) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule4 % 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 squirrel is blue.
("squirrel" "is" "blue" "+")
int4
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int5
The rabbit is not blue.
Unknown
inv-rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit visits the dog.
Unknown
rconc
[@2: The rabbit visits the dog.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("rabbit" "visits" "dog" "+")
The rabbit does not chase the dog.
Unknown
inv-rconc
[@2: The rabbit chases the dog.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("rabbit" "chases" "dog" "-")
The bald eagle is blue.
Unknown
rconc
[@1: The bald eagle is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "blue" "+")
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The bald eagle chases the dog.
Unknown
rconc
[@2: The bald eagle chases the dog.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("bald eagle" "chases" "dog" "+")
The squirrel does not chase the rabbit.
Unknown
inv-random
[@0: The squirrel chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "rabbit" "-")
The dog chases the squirrel.
Unknown
random
[@0: The dog chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "squirrel" "+")
The squirrel does not need the bald eagle.
Unknown
inv-random
[@0: The squirrel needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "bald eagle" "-")
The squirrel chases the bald eagle.
Unknown
random
[@0: The squirrel chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "bald eagle" "+")
The bald eagle does not visit the squirrel.
Unknown
inv-random
[@0: The bald eagle visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "squirrel" "-")
The rabbit needs the dog.
Unknown
random
[@0: The rabbit needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "dog" "+")
@0: The bald eagle is round.[(triple1)] The bald eagle needs the dog.[(triple2)] The bald eagle needs the rabbit.[(triple3)] The bald eagle needs the squirrel.[(triple4)] The bald eagle visits the dog.[(triple5)] The bald eagle visits the rabbit.[(triple6)] The dog chases the rabbit.[(triple7)] The dog is big.[(triple8)] The dog visits the rabbit.[(triple9)] The rabbit needs the bald eagle.[(triple10)] The rabbit visits the squirrel.[(triple11)] The squirrel is big.[(triple12)] The squirrel visits the bald eagle.[(triple13)] The squirrel visits the rabbit.[(triple14)] @1: The dog needs the rabbit.[(((triple8) -> rule1))] The squirrel needs the rabbit.[(((triple12) -> rule1))] @2: The squirrel is blue.[(((((triple12) -> rule1) triple13) -> rule2))] @3: The squirrel chases the dog.[(((((((triple12) -> rule1) triple13) -> rule2)) -> rule5))] The squirrel visits the dog.[(((((((triple12) -> rule1) triple13) -> rule2)) -> rule4))] @4: The dog is blue.[(((triple13 ((((((triple12) -> rule1) triple13) -> rule2)) -> rule4)) -> rule3))] @5: The dog chases the dog.[(((((triple13 ((((((triple12) -> rule1) triple13) -> rule2)) -> rule4)) -> rule3)) -> rule5))] The dog visits the dog.[(((((triple13 ((((((triple12) -> rule1) triple13) -> rule2)) -> rule4)) -> rule3)) -> rule4))]
The bald eagle is round.
("bald eagle" "is" "round" "+")
triple1
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
triple2
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
triple3
The bald eagle needs the squirrel.
("bald eagle" "needs" "squirrel" "+")
triple4
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
triple5
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
triple6
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple7
The dog is big.
("dog" "is" "big" "+")
triple8
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple9
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
triple10
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple11
The squirrel is big.
("squirrel" "is" "big" "+")
triple12
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
triple13
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple14
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
((triple8) -> (rule1 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
((triple12) -> (rule1 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((((triple12) -> (rule1 % int2)) triple13) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int2
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
((((((triple12) -> (rule1 % int3)) triple13) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int3
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
((((((triple12) -> (rule1 % int3)) triple13) -> (rule2 % int2))) -> (rule4 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int3
The dog is blue.
("dog" "is" "blue" "+")
((triple13 ((((((triple12) -> (rule1 % int4)) triple13) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int4
The dog chases the dog.
("dog" "chases" "dog" "+")
((((triple13 ((((((triple12) -> (rule1 % int5)) triple13) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int3
The squirrel is blue.
("squirrel" "is" "blue" "+")
int4
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int5
The dog visits the dog.
("dog" "visits" "dog" "+")
((((triple13 ((((((triple12) -> (rule1 % int5)) triple13) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule4 % 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 squirrel is blue.
("squirrel" "is" "blue" "+")
int4
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int5