The bear is nice. The cow is green. If someone needs the cow then they visit the cow. If someone is green then they need the cow.
The bear is nice.
("bear" "is" "nice" "+")
The cow is green.
("cow" "is" "green" "+")
If someone needs the cow then they visit the cow.
((("someone" "needs" "cow" "+")) -> ("someone" "visits" "cow" "+"))
If someone is green then they need the cow.
((("someone" "is" "green" "+")) -> ("someone" "needs" "cow" "+"))
The bear is nice.
True
1
proof
[(triple1)]
("bear" "is" "nice" "+")
triple1
The bear is not nice.
False
1
inv-proof
[(triple1)]
("bear" "is" "nice" "-")
triple1
The cow needs the cow.
True
2
proof
[(((triple2) -> rule2))]
("cow" "needs" "cow" "+")
((triple2) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not need the cow.
False
2
inv-proof
[(((triple2) -> rule2))]
("cow" "needs" "cow" "-")
((triple2) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow visits the cow.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("cow" "visits" "cow" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow does not visit the cow.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("cow" "visits" "cow" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The bear does not need the cow.
Unknown
inv-rconc
[@1: The bear needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "needs" "cow" "-")
The bear visits the cow.
Unknown
rconc
[@2: The bear visits the cow.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("bear" "visits" "cow" "+")
The cow does not need the bear.
Unknown
inv-random
[@0: The cow needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "bear" "-")
The cow visits the bear.
Unknown
random
[@0: The cow visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "bear" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The bear is nice.[(triple1)] The cow is green.[(triple2)] @1: The cow needs the cow.[(((triple2) -> rule2))] @2: The cow visits the cow.[(((((triple2) -> rule2)) -> rule1))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple2) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2