The bear is young. The cow eats the bear. The cow is nice. If something eats the bear then it chases the cow. If something chases the bear then the bear eats the cow. If something chases the cow then it eats the cow.
The bear is young.
("bear" "is" "young" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow is nice.
("cow" "is" "nice" "+")
If something eats the bear then it chases the cow.
((("something" "eats" "bear" "+")) -> ("something" "chases" "cow" "+"))
If something chases the bear then the bear eats the cow.
((("something" "chases" "bear" "+")) -> ("bear" "eats" "cow" "+"))
If something chases the cow then it eats the cow.
((("something" "chases" "cow" "+")) -> ("something" "eats" "cow" "+"))
The cow eats the bear.
True
1
proof
[(triple2)]
("cow" "eats" "bear" "+")
triple2
The cow does not eat the bear.
False
1
inv-proof
[(triple2)]
("cow" "eats" "bear" "-")
triple2
The cow chases the cow.
True
2
proof
[(((triple2) -> rule1))]
("cow" "chases" "cow" "+")
((triple2) -> (rule1 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow does not chase the cow.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "chases" "cow" "-")
((triple2) -> (rule1 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow eats the cow.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("cow" "eats" "cow" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow does not eat the cow.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("cow" "eats" "cow" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The bear does not chase the cow.
Unknown
inv-rconc
[@1: The bear chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "chases" "cow" "-")
The bear eats the cow.
Unknown
rconc
[@2: The bear eats the cow.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("bear" "eats" "cow" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
The bear does not see the cow.
Unknown
inv-random
[@0: The bear sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "cow" "-")
The cow sees the bear.
Unknown
random
[@0: The cow sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "bear" "+")
@0: The bear is young.[(triple1)] The cow eats the bear.[(triple2)] The cow is nice.[(triple3)] @1: The cow chases the cow.[(((triple2) -> rule1))] @2: The cow eats the cow.[(((((triple2) -> rule1)) -> rule3))]
The bear is young.
("bear" "is" "young" "+")
triple1
The cow eats the bear.
("cow" "eats" "bear" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple2) -> (rule1 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2