The bald eagle is blue. The bald eagle sees the cat. The bald eagle visits the tiger. The cat is green. The cat sees the squirrel. The squirrel needs the cat. The tiger is blue. The tiger is cold. The tiger needs the squirrel. The tiger does not see the bald eagle. The tiger sees the squirrel. The tiger does not visit the cat. If someone sees the tiger then the tiger is green. If someone is nice and green then they see the tiger. If the bald eagle needs the squirrel then the bald eagle is green. If someone sees the cat and they need the cat then the cat needs the squirrel. If someone visits the squirrel and they are not blue then the squirrel does not visit the tiger. If someone is green then they are nice. If someone visits the cat then the cat does not see the squirrel. If someone needs the bald eagle and the bald eagle sees the tiger then the tiger sees the squirrel. If someone visits the tiger and the tiger does not see the cat then the tiger needs the bald eagle.
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
The cat is green.
("cat" "is" "green" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
The tiger does not see the bald eagle.
("tiger" "sees" "bald eagle" "-")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
The tiger does not visit the cat.
("tiger" "visits" "cat" "-")
If someone sees the tiger then the tiger is green.
((("someone" "sees" "tiger" "+")) -> ("tiger" "is" "green" "+"))
If someone is nice and green then they see the tiger.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "sees" "tiger" "+"))
If the bald eagle needs the squirrel then the bald eagle is green.
((("bald eagle" "needs" "squirrel" "+")) -> ("bald eagle" "is" "green" "+"))
If someone sees the cat and they need the cat then the cat needs the squirrel.
((("someone" "sees" "cat" "+") ("someone" "needs" "cat" "+")) -> ("cat" "needs" "squirrel" "+"))
If someone visits the squirrel and they are not blue then the squirrel does not visit the tiger.
((("someone" "visits" "squirrel" "+") ("someone" "is" "blue" "~")) -> ("squirrel" "visits" "tiger" "-"))
If someone is green then they are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone visits the cat then the cat does not see the squirrel.
((("someone" "visits" "cat" "+")) -> ("cat" "sees" "squirrel" "-"))
If someone needs the bald eagle and the bald eagle sees the tiger then the tiger sees the squirrel.
((("someone" "needs" "bald eagle" "+") ("bald eagle" "sees" "tiger" "+")) -> ("tiger" "sees" "squirrel" "+"))
If someone visits the tiger and the tiger does not see the cat then the tiger needs the bald eagle.
((("someone" "visits" "tiger" "+") ("tiger" "sees" "cat" "~")) -> ("tiger" "needs" "bald eagle" "+"))
The tiger does not see the bald eagle.
True
1
proof
[(triple10)]
("tiger" "sees" "bald eagle" "-")
triple10
The squirrel does not need the cat.
False
1
inv-proof
[(triple6)]
("squirrel" "needs" "cat" "-")
triple6
The cat is nice.
True
2
proof
[(((triple4) -> rule6))]
("cat" "is" "nice" "+")
((triple4) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is not nice.
False
2
inv-proof
[(((triple4) -> rule6))]
("cat" "is" "nice" "-")
((triple4) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat sees the tiger.
True
4
proof
[(((((triple4) -> rule6) triple4) -> rule2))]
("cat" "sees" "tiger" "+")
((((triple4) -> (rule6 % int2)) triple4) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat does not see the tiger.
False
4
inv-proof
[(((((triple4) -> rule6) triple4) -> rule2))]
("cat" "sees" "tiger" "-")
((((triple4) -> (rule6 % int2)) triple4) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The tiger is green.
True
5
proof
[(((((((triple4) -> rule6) triple4) -> rule2)) -> rule1))]
("tiger" "is" "green" "+")
((((((triple4) -> (rule6 % int3)) triple4) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The tiger is not green.
False
5
inv-proof
[(((((((triple4) -> rule6) triple4) -> rule2)) -> rule1))]
("tiger" "is" "green" "-")
((((((triple4) -> (rule6 % int3)) triple4) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The tiger is nice.
True
6
proof
[(((((((((triple4) -> rule6) triple4) -> rule2)) -> rule1)) -> rule6))]
("tiger" "is" "nice" "+")
((((((((triple4) -> (rule6 % int4)) triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The cat is nice.
("cat" "is" "nice" "+")
int4
The tiger is not nice.
False
6
inv-proof
[(((((((((triple4) -> rule6) triple4) -> rule2)) -> rule1)) -> rule6))]
("tiger" "is" "nice" "-")
((((((((triple4) -> (rule6 % int4)) triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The cat is nice.
("cat" "is" "nice" "+")
int4
The tiger sees the tiger.
True
12
proof
[(((((((((((triple4) -> rule6) triple4) -> rule2)) -> rule1)) -> rule6) ((((((triple4) -> rule6) triple4) -> rule2)) -> rule1)) -> rule2))]
("tiger" "sees" "tiger" "+")
((((((((((triple4) -> (rule6 % int5)) triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2)) ((((((triple4) -> (rule6 % int5)) triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int4
The cat is nice.
("cat" "is" "nice" "+")
int5
The tiger does not see the tiger.
False
12
inv-proof
[(((((((((((triple4) -> rule6) triple4) -> rule2)) -> rule1)) -> rule6) ((((((triple4) -> rule6) triple4) -> rule2)) -> rule1)) -> rule2))]
("tiger" "sees" "tiger" "-")
((((((((((triple4) -> (rule6 % int5)) triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2)) ((((((triple4) -> (rule6 % int5)) triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int4
The cat is nice.
("cat" "is" "nice" "+")
int5
The cat does not need the squirrel.
Unknown
inv-rconc
[@1: The cat needs the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "needs" "squirrel" "-")
The squirrel sees the tiger.
Unknown
rconc
[@1: The squirrel sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "tiger" "+")
The tiger does not need the bald eagle.
Unknown
inv-rconc
[@1: The tiger needs the bald eagle.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("tiger" "needs" "bald eagle" "-")
The bald eagle is nice.
Unknown
rconc
[@2: The bald eagle is nice.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("bald eagle" "is" "nice" "+")
The squirrel is not nice.
Unknown
inv-rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "nice" "-")
The bald eagle sees the tiger.
Unknown
rconc
[@2: The bald eagle sees the tiger.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("bald eagle" "sees" "tiger" "+")
The tiger does not see the cat.
Unknown
inv-random
[@0: The tiger sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cat" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
The bald eagle does not need the cat.
Unknown
inv-random
[@0: The bald eagle needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "cat" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The cat does not visit the squirrel.
Unknown
inv-random
[@0: The cat visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "squirrel" "-")
The bald eagle is cold.
Unknown
random
[@0: The bald eagle is cold.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "cold" "+")
@0: The bald eagle is blue.[(triple1)] The bald eagle sees the cat.[(triple2)] The bald eagle visits the tiger.[(triple3)] The cat is green.[(triple4)] The cat sees the squirrel.[(triple5)] The squirrel needs the cat.[(triple6)] The tiger does not see the bald eagle.[(triple10)] The tiger does not visit the cat.[(triple12)] The tiger is blue.[(triple7)] The tiger is cold.[(triple8)] The tiger needs the squirrel.[(triple9)] The tiger sees the squirrel.[(triple11)] @1: The cat is nice.[(((triple4) -> rule6))] @2: The cat sees the tiger.[(((((triple4) -> rule6) triple4) -> rule2))] @3: The tiger is green.[(((((((triple4) -> rule6) triple4) -> rule2)) -> rule1))] @4: The tiger is nice.[(((((((((triple4) -> rule6) triple4) -> rule2)) -> rule1)) -> rule6))] @5: The tiger sees the tiger.[(((((((((((triple4) -> rule6) triple4) -> rule2)) -> rule1)) -> rule6) ((((((triple4) -> rule6) triple4) -> rule2)) -> rule1)) -> rule2))]
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
triple1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
triple2
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
triple3
The cat is green.
("cat" "is" "green" "+")
triple4
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple5
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple6
The tiger does not see the bald eagle.
("tiger" "sees" "bald eagle" "-")
triple10
The tiger does not visit the cat.
("tiger" "visits" "cat" "-")
triple12
The tiger is blue.
("tiger" "is" "blue" "+")
triple7
The tiger is cold.
("tiger" "is" "cold" "+")
triple8
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple9
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple11
The cat is nice.
("cat" "is" "nice" "+")
((triple4) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
((((triple4) -> (rule6 % int2)) triple4) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
((((((triple4) -> (rule6 % int3)) triple4) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
((((((((triple4) -> (rule6 % int4)) triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The cat is nice.
("cat" "is" "nice" "+")
int4
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((((((((triple4) -> (rule6 % int5)) triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2)) ((((((triple4) -> (rule6 % int5)) triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int4
The cat is nice.
("cat" "is" "nice" "+")
int5