The bear is big. The bear is not blue. The bear is red. The cow chases the bear. The cow chases the tiger. The cow is blue. The cow is not green. The cow does not like the bear. The cow visits the tiger. The tiger visits the bear. If something likes the bear then the bear visits the cow. If something chases the cow then it is not big. If something likes the cow and it does not chase the bear then it is big. If something likes the tiger and it likes the bear then the bear chases the cow. If something likes the tiger and the tiger is blue then it visits the tiger. If something visits the cow and the cow is not kind then the cow does not chase the tiger. If something visits the cow then it likes the bear. If the cow chases the tiger then the tiger likes the bear.
The bear is big.
("bear" "is" "big" "+")
The bear is not blue.
("bear" "is" "blue" "-")
The bear is red.
("bear" "is" "red" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is not green.
("cow" "is" "green" "-")
The cow does not like the bear.
("cow" "likes" "bear" "-")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If something likes the bear then the bear visits the cow.
((("something" "likes" "bear" "+")) -> ("bear" "visits" "cow" "+"))
If something chases the cow then it is not big.
((("something" "chases" "cow" "+")) -> ("something" "is" "big" "-"))
If something likes the cow and it does not chase the bear then it is big.
((("something" "likes" "cow" "+") ("something" "chases" "bear" "~")) -> ("something" "is" "big" "+"))
If something likes the tiger and it likes the bear then the bear chases the cow.
((("something" "likes" "tiger" "+") ("something" "likes" "bear" "+")) -> ("bear" "chases" "cow" "+"))
If something likes the tiger and the tiger is blue then it visits the tiger.
((("something" "likes" "tiger" "+") ("tiger" "is" "blue" "+")) -> ("something" "visits" "tiger" "+"))
If something visits the cow and the cow is not kind then the cow does not chase the tiger.
((("something" "visits" "cow" "+") ("cow" "is" "kind" "~")) -> ("cow" "chases" "tiger" "-"))
If something visits the cow then it likes the bear.
((("something" "visits" "cow" "+")) -> ("something" "likes" "bear" "+"))
If the cow chases the tiger then the tiger likes the bear.
((("cow" "chases" "tiger" "+")) -> ("tiger" "likes" "bear" "+"))
The tiger visits the bear.
True
1
proof
[(triple10)]
("tiger" "visits" "bear" "+")
triple10
The cow does not chase the bear.
False
1
inv-proof
[(triple4)]
("cow" "chases" "bear" "-")
triple4
The tiger likes the bear.
True
2
proof
[(((triple5) -> rule8))]
("tiger" "likes" "bear" "+")
((triple5) -> (rule8 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger does not like the bear.
False
2
inv-proof
[(((triple5) -> rule8))]
("tiger" "likes" "bear" "-")
((triple5) -> (rule8 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The bear visits the cow.
True
3
proof
[(((((triple5) -> rule8)) -> rule1))]
("bear" "visits" "cow" "+")
((((triple5) -> (rule8 % int2))) -> (rule1 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The bear does not visit the cow.
False
3
inv-proof
[(((((triple5) -> rule8)) -> rule1))]
("bear" "visits" "cow" "-")
((((triple5) -> (rule8 % int2))) -> (rule1 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The bear likes the bear.
True
4
proof
[(((((((triple5) -> rule8)) -> rule1)) -> rule7))]
("bear" "likes" "bear" "+")
((((((triple5) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3
The bear does not like the bear.
False
4
inv-proof
[(((((((triple5) -> rule8)) -> rule1)) -> rule7))]
("bear" "likes" "bear" "-")
((((((triple5) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3
The tiger is not big.
Unknown
inv-rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "big" "-")
The cow is big.
Unknown
rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "big" "+")
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The bear chases the cow.
Unknown
rconc
[@1: The bear chases the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "chases" "cow" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The bear does not like the cow.
Unknown
inv-random
[@0: The bear likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "cow" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The bear is big.[(triple1)] The bear is not blue.[(triple2)] The bear is red.[(triple3)] The cow chases the bear.[(triple4)] The cow chases the tiger.[(triple5)] The cow does not like the bear.[(triple8)] The cow is blue.[(triple6)] The cow is not green.[(triple7)] The cow visits the tiger.[(triple9)] The tiger visits the bear.[(triple10)] @1: The tiger likes the bear.[(((triple5) -> rule8))] @2: The bear visits the cow.[(((((triple5) -> rule8)) -> rule1))] @3: The bear likes the bear.[(((((((triple5) -> rule8)) -> rule1)) -> rule7))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is not blue.
("bear" "is" "blue" "-")
triple2
The bear is red.
("bear" "is" "red" "+")
triple3
The cow chases the bear.
("cow" "chases" "bear" "+")
triple4
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple5
The cow does not like the bear.
("cow" "likes" "bear" "-")
triple8
The cow is blue.
("cow" "is" "blue" "+")
triple6
The cow is not green.
("cow" "is" "green" "-")
triple7
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple9
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple10
The tiger likes the bear.
("tiger" "likes" "bear" "+")
((triple5) -> (rule8 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
((((triple5) -> (rule8 % int2))) -> (rule1 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
((((((triple5) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3