The bald eagle is blue. The bald eagle likes the cat. The bald eagle needs the tiger. The bald eagle does not see the cat. The cat is big. The cat is red. The cat likes the bald eagle. The cow is not blue. The cow likes the bald eagle. The cow likes the cat. The cow needs the bald eagle. The tiger likes the cat. The tiger needs the bald eagle. The tiger needs the cow. The tiger sees the bald eagle. The tiger sees the cat. If something likes the cow and the cow likes the cat then it is cold. If the bald eagle is blue then the bald eagle needs the tiger. Blue, cold things are round. If something needs the tiger and it is round then the tiger is cold. If something is cold then it sees the tiger. If something likes the cat then the cat is blue. If something needs the cow then it does not see the cow. If something sees the bald eagle then the bald eagle likes the cow. If something needs the cat and it is blue then it does not see the cat.
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
The bald eagle does not see the cat.
("bald eagle" "sees" "cat" "-")
The cat is big.
("cat" "is" "big" "+")
The cat is red.
("cat" "is" "red" "+")
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
The cow is not blue.
("cow" "is" "blue" "-")
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If something likes the cow and the cow likes the cat then it is cold.
((("something" "likes" "cow" "+") ("cow" "likes" "cat" "+")) -> ("something" "is" "cold" "+"))
If the bald eagle is blue then the bald eagle needs the tiger.
((("bald eagle" "is" "blue" "+")) -> ("bald eagle" "needs" "tiger" "+"))
Blue, cold things are round.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something needs the tiger and it is round then the tiger is cold.
((("something" "needs" "tiger" "+") ("something" "is" "round" "+")) -> ("tiger" "is" "cold" "+"))
If something is cold then it sees the tiger.
((("something" "is" "cold" "+")) -> ("something" "sees" "tiger" "+"))
If something likes the cat then the cat is blue.
((("something" "likes" "cat" "+")) -> ("cat" "is" "blue" "+"))
If something needs the cow then it does not see the cow.
((("something" "needs" "cow" "+")) -> ("something" "sees" "cow" "-"))
If something sees the bald eagle then the bald eagle likes the cow.
((("something" "sees" "bald eagle" "+")) -> ("bald eagle" "likes" "cow" "+"))
If something needs the cat and it is blue then it does not see the cat.
((("something" "needs" "cat" "+") ("something" "is" "blue" "+")) -> ("something" "sees" "cat" "-"))
The cat likes the bald eagle.
True
1
proof
[(triple7)]
("cat" "likes" "bald eagle" "+")
triple7
The cat is not big.
False
1
inv-proof
[(triple5)]
("cat" "is" "big" "-")
triple5
The bald eagle likes the cow.
True
2
proof
[(((triple15) -> rule8))]
("bald eagle" "likes" "cow" "+")
((triple15) -> (rule8 % int1))
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int1
The cat is not blue.
False
2
inv-proof
[(((triple10) -> rule6) OR ((triple12) -> rule6) OR ((triple2) -> rule6))]
("cat" "is" "blue" "-")
((triple10) -> (rule6 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((triple12) -> (rule6 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((triple2) -> (rule6 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The bald eagle is cold.
True
4
proof
[(((((triple15) -> rule8) triple10) -> rule1))]
("bald eagle" "is" "cold" "+")
((((triple15) -> (rule8 % int2)) triple10) -> (rule1 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int2
The bald eagle is not cold.
False
4
inv-proof
[(((((triple15) -> rule8) triple10) -> rule1))]
("bald eagle" "is" "cold" "-")
((((triple15) -> (rule8 % int2)) triple10) -> (rule1 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int2
The bald eagle is round.
True
6
proof
[(((triple1 ((((triple15) -> rule8) triple10) -> rule1)) -> rule3))]
("bald eagle" "is" "round" "+")
((triple1 ((((triple15) -> (rule8 % int3)) triple10) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle is round.
("bald eagle" "is" "round" "+")
int1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int2
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int3
The bald eagle does not see the tiger.
False
5
inv-proof
[(((((((triple15) -> rule8) triple10) -> rule1)) -> rule5))]
("bald eagle" "sees" "tiger" "-")
((((((triple15) -> (rule8 % int3)) triple10) -> (rule1 % int2))) -> (rule5 % int1))
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int2
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int3
The tiger is cold.
True
8
proof
[(((triple3 ((triple1 ((((triple15) -> rule8) triple10) -> rule1)) -> rule3)) -> rule4) OR ((((triple1) -> rule2) ((triple1 ((((triple15) -> rule8) triple10) -> rule1)) -> rule3)) -> rule4))]
("tiger" "is" "cold" "+")
((triple3 ((triple1 ((((triple15) -> (rule8 % int4)) triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The bald eagle is round.
("bald eagle" "is" "round" "+")
int2
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int3
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int4
((((triple1) -> (rule2 % int5)) ((triple1 ((((triple15) -> (rule8 % int4)) triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The bald eagle is round.
("bald eagle" "is" "round" "+")
int2
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int3
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int4
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int5
The tiger is not cold.
False
8
inv-proof
[(((triple3 ((triple1 ((((triple15) -> rule8) triple10) -> rule1)) -> rule3)) -> rule4) OR ((((triple1) -> rule2) ((triple1 ((((triple15) -> rule8) triple10) -> rule1)) -> rule3)) -> rule4))]
("tiger" "is" "cold" "-")
((triple3 ((triple1 ((((triple15) -> (rule8 % int4)) triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The bald eagle is round.
("bald eagle" "is" "round" "+")
int2
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int3
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int4
((((triple1) -> (rule2 % int5)) ((triple1 ((((triple15) -> (rule8 % int4)) triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The bald eagle is round.
("bald eagle" "is" "round" "+")
int2
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int3
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int4
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int5
The tiger sees the tiger.
True
9
proof
[(((((triple3 ((triple1 ((((triple15) -> rule8) triple10) -> rule1)) -> rule3)) -> rule4)) -> rule5) OR ((((((triple1) -> rule2) ((triple1 ((((triple15) -> rule8) triple10) -> rule1)) -> rule3)) -> rule4)) -> rule5))]
("tiger" "sees" "tiger" "+")
((((triple3 ((triple1 ((((triple15) -> (rule8 % int5)) triple10) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The bald eagle is round.
("bald eagle" "is" "round" "+")
int3
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int4
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int5
((((((triple1) -> (rule2 % int6)) ((triple1 ((((triple15) -> (rule8 % int5)) triple10) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The bald eagle is round.
("bald eagle" "is" "round" "+")
int3
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int4
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int5
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int6
The tiger does not see the tiger.
False
9
inv-proof
[(((((triple3 ((triple1 ((((triple15) -> rule8) triple10) -> rule1)) -> rule3)) -> rule4)) -> rule5) OR ((((((triple1) -> rule2) ((triple1 ((((triple15) -> rule8) triple10) -> rule1)) -> rule3)) -> rule4)) -> rule5))]
("tiger" "sees" "tiger" "-")
((((triple3 ((triple1 ((((triple15) -> (rule8 % int5)) triple10) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The bald eagle is round.
("bald eagle" "is" "round" "+")
int3
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int4
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int5
((((((triple1) -> (rule2 % int6)) ((triple1 ((((triple15) -> (rule8 % int5)) triple10) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The bald eagle is round.
("bald eagle" "is" "round" "+")
int3
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int4
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int5
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int6
The cow is not round.
Unknown
inv-rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "round" "-")
The cow sees the tiger.
Unknown
rconc
[@2: The cow sees the tiger.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("cow" "sees" "tiger" "+")
The cow is not cold.
Unknown
inv-rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "cold" "-")
The cat sees the tiger.
Unknown
rconc
[@2: The cat sees the tiger.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("cat" "sees" "tiger" "+")
The cat is not cold.
Unknown
inv-rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "cold" "-")
The tiger is round.
Unknown
rconc
[@1: The tiger is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "round" "+")
The cow does not need the tiger.
Unknown
inv-random
[@0: The cow needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "tiger" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The tiger needs the cat.
Unknown
random
[@0: The tiger needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "cat" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat sees the cow.
Unknown
random
[@0: The cat sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cow" "+")
@0: The bald eagle does not see the cat.[(triple4)] The bald eagle is blue.[(triple1)] The bald eagle likes the cat.[(triple2)] The bald eagle needs the tiger.[(triple3 OR ((triple1) -> rule2))] The cat is big.[(triple5)] The cat is red.[(triple6)] The cat likes the bald eagle.[(triple7)] The cow is not blue.[(triple8)] The cow likes the bald eagle.[(triple9)] The cow likes the cat.[(triple10)] The cow needs the bald eagle.[(triple11)] The tiger likes the cat.[(triple12)] The tiger needs the bald eagle.[(triple13)] The tiger needs the cow.[(triple14)] The tiger sees the bald eagle.[(triple15)] The tiger sees the cat.[(triple16)] @1: The bald eagle likes the cow.[(((triple15) -> rule8))] The cat is blue.[(((triple10) -> rule6) OR ((triple12) -> rule6) OR ((triple2) -> rule6))] The tiger does not see the cow.[(((triple14) -> rule7))] @2: The bald eagle is cold.[(((((triple15) -> rule8) triple10) -> rule1))] @3: The bald eagle is round.[(((triple1 ((((triple15) -> rule8) triple10) -> rule1)) -> rule3))] The bald eagle sees the tiger.[(((((((triple15) -> rule8) triple10) -> rule1)) -> rule5))] @4: The tiger is cold.[(((triple3 ((triple1 ((((triple15) -> rule8) triple10) -> rule1)) -> rule3)) -> rule4) OR ((((triple1) -> rule2) ((triple1 ((((triple15) -> rule8) triple10) -> rule1)) -> rule3)) -> rule4))] @5: The tiger sees the tiger.[(((((triple3 ((triple1 ((((triple15) -> rule8) triple10) -> rule1)) -> rule3)) -> rule4)) -> rule5) OR ((((((triple1) -> rule2) ((triple1 ((((triple15) -> rule8) triple10) -> rule1)) -> rule3)) -> rule4)) -> rule5))]
The bald eagle does not see the cat.
("bald eagle" "sees" "cat" "-")
triple4
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
triple1
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
triple2
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
triple3
((triple1) -> (rule2 % int1))
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int1
The cat is big.
("cat" "is" "big" "+")
triple5
The cat is red.
("cat" "is" "red" "+")
triple6
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
triple7
The cow is not blue.
("cow" "is" "blue" "-")
triple8
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
triple9
The cow likes the cat.
("cow" "likes" "cat" "+")
triple10
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
triple11
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple12
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
triple13
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple14
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
triple15
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple16
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
((triple15) -> (rule8 % int1))
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((triple10) -> (rule6 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((triple12) -> (rule6 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((triple2) -> (rule6 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The tiger does not see the cow.
("tiger" "sees" "cow" "-")
((triple14) -> (rule7 % int1))
The tiger does not see the cow.
("tiger" "sees" "cow" "-")
int1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
((((triple15) -> (rule8 % int2)) triple10) -> (rule1 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int2
The bald eagle is round.
("bald eagle" "is" "round" "+")
((triple1 ((((triple15) -> (rule8 % int3)) triple10) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle is round.
("bald eagle" "is" "round" "+")
int1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int2
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int3
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
((((((triple15) -> (rule8 % int3)) triple10) -> (rule1 % int2))) -> (rule5 % int1))
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int2
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
((triple3 ((triple1 ((((triple15) -> (rule8 % int4)) triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The bald eagle is round.
("bald eagle" "is" "round" "+")
int2
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int3
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int4
((((triple1) -> (rule2 % int5)) ((triple1 ((((triple15) -> (rule8 % int4)) triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The bald eagle is round.
("bald eagle" "is" "round" "+")
int2
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int3
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int4
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int5
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((triple3 ((triple1 ((((triple15) -> (rule8 % int5)) triple10) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The bald eagle is round.
("bald eagle" "is" "round" "+")
int3
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int4
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int5
((((((triple1) -> (rule2 % int6)) ((triple1 ((((triple15) -> (rule8 % int5)) triple10) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The bald eagle is round.
("bald eagle" "is" "round" "+")
int3
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int4
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int5
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int6