The bear is big. The cow likes the bear. The squirrel visits the cow. If the bear visits the cow and the bear does not like the squirrel then the squirrel is not blue. If something visits the bear and the bear likes the squirrel then the bear visits the squirrel. If something is blue then it visits the squirrel. If something likes the squirrel and it is not big then the squirrel visits the cow. If something likes the bear then it is blue. If something needs the bear then it visits the bear. If the squirrel does not visit the cow and the cow is not blue then the cow is cold. If something likes the bear and it does not visit the squirrel then it needs the cow.
The bear is big.
("bear" "is" "big" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If the bear visits the cow and the bear does not like the squirrel then the squirrel is not blue.
((("bear" "visits" "cow" "+") ("bear" "likes" "squirrel" "~")) -> ("squirrel" "is" "blue" "-"))
If something visits the bear and the bear likes the squirrel then the bear visits the squirrel.
((("something" "visits" "bear" "+") ("bear" "likes" "squirrel" "+")) -> ("bear" "visits" "squirrel" "+"))
If something is blue then it visits the squirrel.
((("something" "is" "blue" "+")) -> ("something" "visits" "squirrel" "+"))
If something likes the squirrel and it is not big then the squirrel visits the cow.
((("something" "likes" "squirrel" "+") ("something" "is" "big" "~")) -> ("squirrel" "visits" "cow" "+"))
If something likes the bear then it is blue.
((("something" "likes" "bear" "+")) -> ("something" "is" "blue" "+"))
If something needs the bear then it visits the bear.
((("something" "needs" "bear" "+")) -> ("something" "visits" "bear" "+"))
If the squirrel does not visit the cow and the cow is not blue then the cow is cold.
((("squirrel" "visits" "cow" "~") ("cow" "is" "blue" "~")) -> ("cow" "is" "cold" "+"))
If something likes the bear and it does not visit the squirrel then it needs the cow.
((("something" "likes" "bear" "+") ("something" "visits" "squirrel" "~")) -> ("something" "needs" "cow" "+"))
The cow likes the bear.
True
1
proof
[(triple2)]
("cow" "likes" "bear" "+")
triple2
The squirrel does not visit the cow.
False
1
inv-proof
[(triple3)]
("squirrel" "visits" "cow" "-")
triple3
The cow is blue.
True
2
proof
[(((triple2) -> rule5))]
("cow" "is" "blue" "+")
((triple2) -> (rule5 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is not blue.
False
2
inv-proof
[(((triple2) -> rule5))]
("cow" "is" "blue" "-")
((triple2) -> (rule5 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow visits the squirrel.
True
3
proof
[(((((triple2) -> rule5)) -> rule3))]
("cow" "visits" "squirrel" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow does not visit the squirrel.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule3))]
("cow" "visits" "squirrel" "-")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The bear does not visit the squirrel.
Unknown
inv-rconc
[@2: The bear visits the squirrel.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("bear" "visits" "squirrel" "-")
The squirrel is blue.
Unknown
rconc
[@1: The squirrel is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "blue" "+")
The cow is not cold.
Unknown
inv-rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "is" "cold" "-")
The bear likes the cow.
Unknown
random
[@0: The bear likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "cow" "+")
The squirrel does not need the bear.
Unknown
inv-random
[@0: The squirrel needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "bear" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The bear is big.[(triple1)] The cow likes the bear.[(triple2)] The squirrel visits the cow.[(triple3)] @1: The cow is blue.[(((triple2) -> rule5))] @2: The cow visits the squirrel.[(((((triple2) -> rule5)) -> rule3))]
The bear is big.
("bear" "is" "big" "+")
triple1
The cow likes the bear.
("cow" "likes" "bear" "+")
triple2
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple3
The cow is blue.
("cow" "is" "blue" "+")
((triple2) -> (rule5 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2