The bear eats the cow. The cow is rough. If something visits the cow then it is not blue. If the bear is not rough then the bear is blue. If the bear is not big then the bear eats the cow. If something is nice then it eats the cow. All rough things are nice. If something visits the bear then the bear chases the cow.
The bear eats the cow.
("bear" "eats" "cow" "+")
The cow is rough.
("cow" "is" "rough" "+")
If something visits the cow then it is not blue.
((("something" "visits" "cow" "+")) -> ("something" "is" "blue" "-"))
If the bear is not rough then the bear is blue.
((("bear" "is" "rough" "~")) -> ("bear" "is" "blue" "+"))
If the bear is not big then the bear eats the cow.
((("bear" "is" "big" "~")) -> ("bear" "eats" "cow" "+"))
If something is nice then it eats the cow.
((("something" "is" "nice" "+")) -> ("something" "eats" "cow" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something visits the bear then the bear chases the cow.
((("something" "visits" "bear" "+")) -> ("bear" "chases" "cow" "+"))
The cow is rough.
True
1
proof
[(triple2)]
("cow" "is" "rough" "+")
triple2
The cow is not rough.
False
1
inv-proof
[(triple2)]
("cow" "is" "rough" "-")
triple2
The cow is nice.
True
2
proof
[(((triple2) -> rule5))]
("cow" "is" "nice" "+")
((triple2) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is not nice.
False
2
inv-proof
[(((triple2) -> rule5))]
("cow" "is" "nice" "-")
((triple2) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow eats the cow.
True
3
proof
[(((((triple2) -> rule5)) -> rule4))]
("cow" "eats" "cow" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow does not eat the cow.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule4))]
("cow" "eats" "cow" "-")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The bear does not chase the cow.
Unknown
inv-rconc
[@1: The bear chases the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "chases" "cow" "-")
The bear is nice.
Unknown
rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "nice" "+")
The bear is not blue.
Unknown
inv-rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "blue" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
@0: The bear eats the cow.[(triple1)] The cow is rough.[(triple2)] @1: The cow is nice.[(((triple2) -> rule5))] @2: The cow eats the cow.[(((((triple2) -> rule5)) -> rule4))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
((triple2) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2