The bald eagle needs the cat. The cat needs the bald eagle. The mouse needs the squirrel. The mouse visits the cat. The squirrel is big. The squirrel is cold. The squirrel visits the bald eagle. If something needs the squirrel then it is cold. If something visits the cat then it is big. If something needs the squirrel and it is cold then the squirrel visits the cat.
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
If something needs the squirrel then it is cold.
((("something" "needs" "squirrel" "+")) -> ("something" "is" "cold" "+"))
If something visits the cat then it is big.
((("something" "visits" "cat" "+")) -> ("something" "is" "big" "+"))
If something needs the squirrel and it is cold then the squirrel visits the cat.
((("something" "needs" "squirrel" "+") ("something" "is" "cold" "+")) -> ("squirrel" "visits" "cat" "+"))
The mouse needs the squirrel.
True
1
proof
[(triple3)]
("mouse" "needs" "squirrel" "+")
triple3
The squirrel does not visit the bald eagle.
False
1
inv-proof
[(triple7)]
("squirrel" "visits" "bald eagle" "-")
triple7
The mouse is big.
True
2
proof
[(((triple4) -> rule2))]
("mouse" "is" "big" "+")
((triple4) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is not cold.
False
2
inv-proof
[(((triple3) -> rule1))]
("mouse" "is" "cold" "-")
((triple3) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The squirrel visits the cat.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule3))]
("squirrel" "visits" "cat" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The squirrel does not visit the cat.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule3))]
("squirrel" "visits" "cat" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The cat is not big.
Unknown
inv-rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "big" "-")
The cat is cold.
Unknown
rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "cold" "+")
The bald eagle is not big.
Unknown
inv-rconc
[@1: The bald eagle is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "big" "-")
The bald eagle visits the mouse.
Unknown
random
[@0: The bald eagle visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "mouse" "+")
The mouse is not nice.
Unknown
inv-random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "-")
The cat visits the squirrel.
Unknown
random
[@0: The cat visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "squirrel" "+")
@0: The bald eagle needs the cat.[(triple1)] The cat needs the bald eagle.[(triple2)] The mouse needs the squirrel.[(triple3)] The mouse visits the cat.[(triple4)] The squirrel is big.[(triple5 OR ((((triple3 ((triple3) -> rule1)) -> rule3)) -> rule2))] The squirrel is cold.[(triple6)] The squirrel visits the bald eagle.[(triple7)] @1: The mouse is big.[(((triple4) -> rule2))] The mouse is cold.[(((triple3) -> rule1))] @2: The squirrel visits the cat.[(((triple3 ((triple3) -> rule1)) -> rule3))]
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
triple1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
triple2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple3
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple4
The squirrel is big.
("squirrel" "is" "big" "+")
triple5
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple6
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
triple7
The mouse is big.
("mouse" "is" "big" "+")
((triple4) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((triple3) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2