The bear eats the cow. The bear eats the tiger. The bear is cold. The cow eats the bear. The cow is nice. The cow is red. The cow sees the bear. The tiger eats the cow. The tiger is cold. The tiger is red. The tiger needs the bear. The tiger needs the cow. If the tiger is nice then the tiger sees the bear. If something is cold then it is young. If something is young and red then it sees the cow.
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear is cold.
("bear" "is" "cold" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
If the tiger is nice then the tiger sees the bear.
((("tiger" "is" "nice" "+")) -> ("tiger" "sees" "bear" "+"))
If something is cold then it is young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something is young and red then it sees the cow.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "sees" "cow" "+"))
The bear eats the tiger.
True
1
proof
[(triple2)]
("bear" "eats" "tiger" "+")
triple2
The cow does not see the bear.
False
1
inv-proof
[(triple7)]
("cow" "sees" "bear" "-")
triple7
The tiger is young.
True
2
proof
[(((triple9) -> rule2))]
("tiger" "is" "young" "+")
((triple9) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The bear is not young.
False
2
inv-proof
[(((triple3) -> rule2))]
("bear" "is" "young" "-")
((triple3) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "young" "-")
The tiger sees the bear.
Unknown
rconc
[@1: The tiger sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "bear" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "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 eats the cow.[(triple1)] The bear eats the tiger.[(triple2)] The bear is cold.[(triple3)] The cow eats the bear.[(triple4)] The cow is nice.[(triple5)] The cow is red.[(triple6)] The cow sees the bear.[(triple7)] The tiger eats the cow.[(triple8)] The tiger is cold.[(triple9)] The tiger is red.[(triple10)] The tiger needs the bear.[(triple11)] The tiger needs the cow.[(triple12)] @1: The bear is young.[(((triple3) -> rule2))] The tiger is young.[(((triple9) -> rule2))] @2: The tiger sees the cow.[(((((triple9) -> rule2) triple10) -> rule3))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple2
The bear is cold.
("bear" "is" "cold" "+")
triple3
The cow eats the bear.
("cow" "eats" "bear" "+")
triple4
The cow is nice.
("cow" "is" "nice" "+")
triple5
The cow is red.
("cow" "is" "red" "+")
triple6
The cow sees the bear.
("cow" "sees" "bear" "+")
triple7
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple8
The tiger is cold.
("tiger" "is" "cold" "+")
triple9
The tiger is red.
("tiger" "is" "red" "+")
triple10
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple11
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple12
The bear is young.
("bear" "is" "young" "+")
((triple3) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
((triple9) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
((((triple9) -> (rule2 % int2)) triple10) -> (rule3 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2