The bald eagle needs the mouse. The cat is blue. The cat likes the bald eagle. The cat likes the cow. The cat needs the cow. The cat sees the bald eagle. The cow is cold. The cow likes the cat. The cow sees the mouse. The mouse needs the cat. If something sees the mouse then it likes the bald eagle. If something is cold then it sees the cow. If something sees the mouse and it is cold then the mouse likes the cat. If something needs the mouse and the mouse likes the cow then the mouse needs the cow. If something is cold and it needs the mouse then the mouse sees the cat. If something sees the cat and the cat needs the cow then it is cold. If something sees the mouse and it needs the cow then the mouse likes the cow. If something likes the bald eagle then it needs the mouse.
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
If something sees the mouse then it likes the bald eagle.
((("something" "sees" "mouse" "+")) -> ("something" "likes" "bald eagle" "+"))
If something is cold then it sees the cow.
((("something" "is" "cold" "+")) -> ("something" "sees" "cow" "+"))
If something sees the mouse and it is cold then the mouse likes the cat.
((("something" "sees" "mouse" "+") ("something" "is" "cold" "+")) -> ("mouse" "likes" "cat" "+"))
If something needs the mouse and the mouse likes the cow then the mouse needs the cow.
((("something" "needs" "mouse" "+") ("mouse" "likes" "cow" "+")) -> ("mouse" "needs" "cow" "+"))
If something is cold and it needs the mouse then the mouse sees the cat.
((("something" "is" "cold" "+") ("something" "needs" "mouse" "+")) -> ("mouse" "sees" "cat" "+"))
If something sees the cat and the cat needs the cow then it is cold.
((("something" "sees" "cat" "+") ("cat" "needs" "cow" "+")) -> ("something" "is" "cold" "+"))
If something sees the mouse and it needs the cow then the mouse likes the cow.
((("something" "sees" "mouse" "+") ("something" "needs" "cow" "+")) -> ("mouse" "likes" "cow" "+"))
If something likes the bald eagle then it needs the mouse.
((("something" "likes" "bald eagle" "+")) -> ("something" "needs" "mouse" "+"))
The cat is blue.
True
1
proof
[(triple2)]
("cat" "is" "blue" "+")
triple2
The mouse does not need the cat.
False
1
inv-proof
[(triple10)]
("mouse" "needs" "cat" "-")
triple10
The cow likes the bald eagle.
True
2
proof
[(((triple9) -> rule1))]
("cow" "likes" "bald eagle" "+")
((triple9) -> (rule1 % int1))
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int1
The mouse does not like the cat.
False
3
inv-proof
[(((triple9 triple7) -> rule3))]
("mouse" "likes" "cat" "-")
((triple9 triple7) -> (rule3 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The cow needs the mouse.
True
3
proof
[(((((triple9) -> rule1)) -> rule8))]
("cow" "needs" "mouse" "+")
((((triple9) -> (rule1 % int2))) -> (rule8 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int2
The cow does not need the mouse.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule8))]
("cow" "needs" "mouse" "-")
((((triple9) -> (rule1 % int2))) -> (rule8 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int2
The mouse sees the cat.
True
5
proof
[(((triple7 ((((triple9) -> rule1)) -> rule8)) -> rule5))]
("mouse" "sees" "cat" "+")
((triple7 ((((triple9) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int3
The mouse does not see the cat.
False
5
inv-proof
[(((triple7 ((((triple9) -> rule1)) -> rule8)) -> rule5))]
("mouse" "sees" "cat" "-")
((triple7 ((((triple9) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int3
The mouse is cold.
True
7
proof
[(((((triple7 ((((triple9) -> rule1)) -> rule8)) -> rule5) triple5) -> rule6))]
("mouse" "is" "cold" "+")
((((triple7 ((((triple9) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule5 % int2)) triple5) -> (rule6 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int4
The mouse is not cold.
False
7
inv-proof
[(((((triple7 ((((triple9) -> rule1)) -> rule8)) -> rule5) triple5) -> rule6))]
("mouse" "is" "cold" "-")
((((triple7 ((((triple9) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule5 % int2)) triple5) -> (rule6 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int4
The mouse sees the cow.
True
8
proof
[(((((((triple7 ((((triple9) -> rule1)) -> rule8)) -> rule5) triple5) -> rule6)) -> rule2))]
("mouse" "sees" "cow" "+")
((((((triple7 ((((triple9) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule5 % int3)) triple5) -> (rule6 % int2))) -> (rule2 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int4
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int5
The mouse does not see the cow.
False
8
inv-proof
[(((((((triple7 ((((triple9) -> rule1)) -> rule8)) -> rule5) triple5) -> rule6)) -> rule2))]
("mouse" "sees" "cow" "-")
((((((triple7 ((((triple9) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule5 % int3)) triple5) -> (rule6 % int2))) -> (rule2 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int4
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int5
The bald eagle is not cold.
Unknown
inv-rconc
[@1: The bald eagle is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "is" "cold" "-")
The bald eagle likes the bald eagle.
Unknown
rconc
[@1: The bald eagle likes the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "likes" "bald eagle" "+")
The mouse does not need the cow.
Unknown
inv-rconc
[@2: The mouse needs the cow.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("mouse" "needs" "cow" "-")
The mouse needs the mouse.
Unknown
rconc
[@2: The mouse needs the mouse.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("mouse" "needs" "mouse" "+")
The cat does not see the cow.
Unknown
inv-rconc
[@2: The cat sees the cow.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("cat" "sees" "cow" "-")
The cat is cold.
Unknown
rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "cold" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
The cow does not need the bald eagle.
Unknown
inv-random
[@0: The cow needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "bald eagle" "-")
The bald eagle likes the mouse.
Unknown
random
[@0: The bald eagle likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "likes" "mouse" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The cow sees the bald eagle.
Unknown
random
[@0: The cow sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "bald eagle" "+")
@0: The bald eagle needs the mouse.[(triple1)] The cat is blue.[(triple2)] The cat likes the bald eagle.[(triple3)] The cat likes the cow.[(triple4)] The cat needs the cow.[(triple5)] The cat sees the bald eagle.[(triple6)] The cow is cold.[(triple7)] The cow likes the cat.[(triple8)] The cow sees the mouse.[(triple9)] The mouse needs the cat.[(triple10)] @1: The cat needs the mouse.[(((triple3) -> rule8))] The cow likes the bald eagle.[(((triple9) -> rule1))] The cow sees the cow.[(((triple7) -> rule2))] The mouse likes the cat.[(((triple9 triple7) -> rule3))] @2: The cow needs the mouse.[(((((triple9) -> rule1)) -> rule8))] @3: The mouse sees the cat.[(((triple7 ((((triple9) -> rule1)) -> rule8)) -> rule5))] @4: The mouse is cold.[(((((triple7 ((((triple9) -> rule1)) -> rule8)) -> rule5) triple5) -> rule6))] @5: The mouse sees the cow.[(((((((triple7 ((((triple9) -> rule1)) -> rule8)) -> rule5) triple5) -> rule6)) -> rule2))]
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
triple3
The cat likes the cow.
("cat" "likes" "cow" "+")
triple4
The cat needs the cow.
("cat" "needs" "cow" "+")
triple5
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
triple6
The cow is cold.
("cow" "is" "cold" "+")
triple7
The cow likes the cat.
("cow" "likes" "cat" "+")
triple8
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple9
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple10
The cat needs the mouse.
("cat" "needs" "mouse" "+")
((triple3) -> (rule8 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
((triple9) -> (rule1 % int1))
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple7) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
((triple9 triple7) -> (rule3 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((((triple9) -> (rule1 % int2))) -> (rule8 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
((triple7 ((((triple9) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
((((triple7 ((((triple9) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule5 % int2)) triple5) -> (rule6 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int4
The mouse sees the cow.
("mouse" "sees" "cow" "+")
((((((triple7 ((((triple9) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule5 % int3)) triple5) -> (rule6 % int2))) -> (rule2 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int4
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int5