The bear eats the cow. The bear sees the tiger. The bear visits the tiger. The cow eats the bear. The cow is green. The cow sees the bear. The tiger eats the cow. If something sees the cow then the cow sees the bear. If the tiger does not eat the cow then the cow eats the tiger. If something is blue and it does not see the bear then it visits the tiger. If something sees the bear and the bear visits the cow then the cow visits the tiger. If something visits the tiger then it visits the cow. If something is young and it sees the cow then it visits the cow.
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow is green.
("cow" "is" "green" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
If something sees the cow then the cow sees the bear.
((("something" "sees" "cow" "+")) -> ("cow" "sees" "bear" "+"))
If the tiger does not eat the cow then the cow eats the tiger.
((("tiger" "eats" "cow" "~")) -> ("cow" "eats" "tiger" "+"))
If something is blue and it does not see the bear then it visits the tiger.
((("something" "is" "blue" "+") ("something" "sees" "bear" "~")) -> ("something" "visits" "tiger" "+"))
If something sees the bear and the bear visits the cow then the cow visits the tiger.
((("something" "sees" "bear" "+") ("bear" "visits" "cow" "+")) -> ("cow" "visits" "tiger" "+"))
If something visits the tiger then it visits the cow.
((("something" "visits" "tiger" "+")) -> ("something" "visits" "cow" "+"))
If something is young and it sees the cow then it visits the cow.
((("something" "is" "young" "+") ("something" "sees" "cow" "+")) -> ("something" "visits" "cow" "+"))
The bear sees the tiger.
True
1
proof
[(triple2)]
("bear" "sees" "tiger" "+")
triple2
The cow is not green.
False
1
inv-proof
[(triple5)]
("cow" "is" "green" "-")
triple5
The bear visits the cow.
True
2
proof
[(((triple3) -> rule5))]
("bear" "visits" "cow" "+")
((triple3) -> (rule5 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
The bear does not visit the cow.
False
2
inv-proof
[(((triple3) -> rule5))]
("bear" "visits" "cow" "-")
((triple3) -> (rule5 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
The cow visits the tiger.
True
4
proof
[(((triple6 ((triple3) -> rule5)) -> rule4))]
("cow" "visits" "tiger" "+")
((triple6 ((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
int2
The cow does not visit the tiger.
False
4
inv-proof
[(((triple6 ((triple3) -> rule5)) -> rule4))]
("cow" "visits" "tiger" "-")
((triple6 ((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
int2
The cow visits the cow.
True
5
proof
[(((((triple6 ((triple3) -> rule5)) -> rule4)) -> rule5))]
("cow" "visits" "cow" "+")
((((triple6 ((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
int3
The cow does not visit the cow.
False
5
inv-proof
[(((((triple6 ((triple3) -> rule5)) -> rule4)) -> rule5))]
("cow" "visits" "cow" "-")
((((triple6 ((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
int3
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The cow eats the tiger.
Unknown
rconc
[@1: The cow eats the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "eats" "tiger" "+")
The tiger does not visit the cow.
Unknown
inv-rconc
[@2: The tiger visits the cow.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("tiger" "visits" "cow" "-")
The tiger eats the bear.
Unknown
random
[@0: The tiger eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "bear" "+")
The tiger does not see the cow.
Unknown
inv-random
[@0: The tiger sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cow" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
@0: The bear eats the cow.[(triple1)] The bear sees the tiger.[(triple2)] The bear visits the tiger.[(triple3)] The cow eats the bear.[(triple4)] The cow is green.[(triple5)] The cow sees the bear.[(triple6)] The tiger eats the cow.[(triple7)] @1: The bear visits the cow.[(((triple3) -> rule5))] @2: The cow visits the tiger.[(((triple6 ((triple3) -> rule5)) -> rule4))] @3: The cow visits the cow.[(((((triple6 ((triple3) -> rule5)) -> rule4)) -> rule5))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple2
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple3
The cow eats the bear.
("cow" "eats" "bear" "+")
triple4
The cow is green.
("cow" "is" "green" "+")
triple5
The cow sees the bear.
("cow" "sees" "bear" "+")
triple6
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple7
The bear visits the cow.
("bear" "visits" "cow" "+")
((triple3) -> (rule5 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
((triple6 ((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple6 ((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
int3