The bear likes the cow. The cow is blue. The cow is nice. If the cow eats the bear then the cow chases the bear. If something chases the bear and it chases the cow then the bear is blue. All red things are young. If the cow is nice then the cow eats the bear. If the cow chases the bear and the cow is young then the cow likes the bear. If something chases the bear then it eats the cow.
The bear likes the cow.
("bear" "likes" "cow" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is nice.
("cow" "is" "nice" "+")
If the cow eats the bear then the cow chases the bear.
((("cow" "eats" "bear" "+")) -> ("cow" "chases" "bear" "+"))
If something chases the bear and it chases the cow then the bear is blue.
((("something" "chases" "bear" "+") ("something" "chases" "cow" "+")) -> ("bear" "is" "blue" "+"))
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If the cow is nice then the cow eats the bear.
((("cow" "is" "nice" "+")) -> ("cow" "eats" "bear" "+"))
If the cow chases the bear and the cow is young then the cow likes the bear.
((("cow" "chases" "bear" "+") ("cow" "is" "young" "+")) -> ("cow" "likes" "bear" "+"))
If something chases the bear then it eats the cow.
((("something" "chases" "bear" "+")) -> ("something" "eats" "cow" "+"))
The cow is nice.
True
1
proof
[(triple3)]
("cow" "is" "nice" "+")
triple3
The bear does not like the cow.
False
1
inv-proof
[(triple1)]
("bear" "likes" "cow" "-")
triple1
The cow eats the bear.
True
2
proof
[(((triple3) -> rule4))]
("cow" "eats" "bear" "+")
((triple3) -> (rule4 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The cow does not eat the bear.
False
2
inv-proof
[(((triple3) -> rule4))]
("cow" "eats" "bear" "-")
((triple3) -> (rule4 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The cow chases the bear.
True
3
proof
[(((((triple3) -> rule4)) -> rule1))]
("cow" "chases" "bear" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The cow does not chase the bear.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule1))]
("cow" "chases" "bear" "-")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The cow eats the cow.
True
4
proof
[(((((((triple3) -> rule4)) -> rule1)) -> rule6))]
("cow" "eats" "cow" "+")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
int2
The cow eats the bear.
("cow" "eats" "bear" "+")
int3
The cow does not eat the cow.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule1)) -> rule6))]
("cow" "eats" "cow" "-")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
int2
The cow eats the bear.
("cow" "eats" "bear" "+")
int3
The bear is not young.
Unknown
inv-rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "young" "-")
The bear is blue.
Unknown
rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "blue" "+")
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "young" "-")
The cow likes the bear.
Unknown
rconc
[@2: The cow likes the bear.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("cow" "likes" "bear" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
The bear does not chase the cow.
Unknown
inv-random
[@0: The bear chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "cow" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
@0: The bear likes the cow.[(triple1)] The cow is blue.[(triple2)] The cow is nice.[(triple3)] @1: The cow eats the bear.[(((triple3) -> rule4))] @2: The cow chases the bear.[(((((triple3) -> rule4)) -> rule1))] @3: The cow eats the cow.[(((((((triple3) -> rule4)) -> rule1)) -> rule6))]
The bear likes the cow.
("bear" "likes" "cow" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow eats the bear.
("cow" "eats" "bear" "+")
((triple3) -> (rule4 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
int2
The cow eats the bear.
("cow" "eats" "bear" "+")
int3