The bear eats the cow. The bear is blue. The bear visits the cow. The cow is big. The cow visits the lion. The lion eats the bear. The tiger visits the bear. If the tiger visits the bear and the tiger eats the bear then the bear chases the lion. If someone chases the cow then they are blue. If someone visits the cow then they chase the bear. If someone eats the bear and the bear is young then they are red. If someone chases the bear and the bear chases the tiger then the bear chases the lion. If someone eats the lion and the lion eats the tiger then they visit the tiger. If someone eats the cow and they chase the bear then they chase the tiger. If the bear is blue and the bear chases the lion then the lion chases the cow. If someone chases the cow and they eat the tiger then the tiger visits the cow.
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear visits the cow.
("bear" "visits" "cow" "+")
The cow is big.
("cow" "is" "big" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If the tiger visits the bear and the tiger eats the bear then the bear chases the lion.
((("tiger" "visits" "bear" "+") ("tiger" "eats" "bear" "+")) -> ("bear" "chases" "lion" "+"))
If someone chases the cow then they are blue.
((("someone" "chases" "cow" "+")) -> ("someone" "is" "blue" "+"))
If someone visits the cow then they chase the bear.
((("someone" "visits" "cow" "+")) -> ("someone" "chases" "bear" "+"))
If someone eats the bear and the bear is young then they are red.
((("someone" "eats" "bear" "+") ("bear" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone chases the bear and the bear chases the tiger then the bear chases the lion.
((("someone" "chases" "bear" "+") ("bear" "chases" "tiger" "+")) -> ("bear" "chases" "lion" "+"))
If someone eats the lion and the lion eats the tiger then they visit the tiger.
((("someone" "eats" "lion" "+") ("lion" "eats" "tiger" "+")) -> ("someone" "visits" "tiger" "+"))
If someone eats the cow and they chase the bear then they chase the tiger.
((("someone" "eats" "cow" "+") ("someone" "chases" "bear" "+")) -> ("someone" "chases" "tiger" "+"))
If the bear is blue and the bear chases the lion then the lion chases the cow.
((("bear" "is" "blue" "+") ("bear" "chases" "lion" "+")) -> ("lion" "chases" "cow" "+"))
If someone chases the cow and they eat the tiger then the tiger visits the cow.
((("someone" "chases" "cow" "+") ("someone" "eats" "tiger" "+")) -> ("tiger" "visits" "cow" "+"))
The bear eats the cow.
True
1
proof
[(triple1)]
("bear" "eats" "cow" "+")
triple1
The bear does not visit the cow.
False
1
inv-proof
[(triple3)]
("bear" "visits" "cow" "-")
triple3
The bear chases the bear.
True
2
proof
[(((triple3) -> rule3))]
("bear" "chases" "bear" "+")
((triple3) -> (rule3 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear does not chase the bear.
False
2
inv-proof
[(((triple3) -> rule3))]
("bear" "chases" "bear" "-")
((triple3) -> (rule3 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear chases the tiger.
True
4
proof
[(((triple1 ((triple3) -> rule3)) -> rule7))]
("bear" "chases" "tiger" "+")
((triple1 ((triple3) -> (rule3 % int2))) -> (rule7 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear does not chase the tiger.
False
4
inv-proof
[(((triple1 ((triple3) -> rule3)) -> rule7))]
("bear" "chases" "tiger" "-")
((triple1 ((triple3) -> (rule3 % int2))) -> (rule7 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear chases the lion.
True
7
proof
[(((((triple3) -> rule3) ((triple1 ((triple3) -> rule3)) -> rule7)) -> rule5))]
("bear" "chases" "lion" "+")
((((triple3) -> (rule3 % int3)) ((triple1 ((triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear chases the bear.
("bear" "chases" "bear" "+")
int3
The bear does not chase the lion.
False
7
inv-proof
[(((((triple3) -> rule3) ((triple1 ((triple3) -> rule3)) -> rule7)) -> rule5))]
("bear" "chases" "lion" "-")
((((triple3) -> (rule3 % int3)) ((triple1 ((triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear chases the bear.
("bear" "chases" "bear" "+")
int3
The lion chases the cow.
True
9
proof
[(((triple2 ((((triple3) -> rule3) ((triple1 ((triple3) -> rule3)) -> rule7)) -> rule5)) -> rule8))]
("lion" "chases" "cow" "+")
((triple2 ((((triple3) -> (rule3 % int4)) ((triple1 ((triple3) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The bear chases the lion.
("bear" "chases" "lion" "+")
int2
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int3
The bear chases the bear.
("bear" "chases" "bear" "+")
int4
The lion does not chase the cow.
False
9
inv-proof
[(((triple2 ((((triple3) -> rule3) ((triple1 ((triple3) -> rule3)) -> rule7)) -> rule5)) -> rule8))]
("lion" "chases" "cow" "-")
((triple2 ((((triple3) -> (rule3 % int4)) ((triple1 ((triple3) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The bear chases the lion.
("bear" "chases" "lion" "+")
int2
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int3
The bear chases the bear.
("bear" "chases" "bear" "+")
int4
The lion is blue.
True
10
proof
[(((((triple2 ((((triple3) -> rule3) ((triple1 ((triple3) -> rule3)) -> rule7)) -> rule5)) -> rule8)) -> rule2))]
("lion" "is" "blue" "+")
((((triple2 ((((triple3) -> (rule3 % int5)) ((triple1 ((triple3) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The bear chases the lion.
("bear" "chases" "lion" "+")
int3
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int4
The bear chases the bear.
("bear" "chases" "bear" "+")
int5
The lion is not blue.
False
10
inv-proof
[(((((triple2 ((((triple3) -> rule3) ((triple1 ((triple3) -> rule3)) -> rule7)) -> rule5)) -> rule8)) -> rule2))]
("lion" "is" "blue" "-")
((((triple2 ((((triple3) -> (rule3 % int5)) ((triple1 ((triple3) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The bear chases the lion.
("bear" "chases" "lion" "+")
int3
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int4
The bear chases the bear.
("bear" "chases" "bear" "+")
int5
The lion is not red.
Unknown
inv-rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "red" "-")
The tiger is red.
Unknown
rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "red" "+")
The lion does not chase the bear.
Unknown
inv-rconc
[@1: The lion chases the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "chases" "bear" "-")
The cow visits the tiger.
Unknown
rconc
[@1: The cow visits the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "visits" "tiger" "+")
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The lion visits the tiger.
Unknown
rconc
[@1: The lion visits the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "visits" "tiger" "+")
The lion does not eat the tiger.
Unknown
inv-random
[@0: The lion eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "tiger" "-")
The cow eats the lion.
Unknown
random
[@0: The cow eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "lion" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The tiger eats the bear.
Unknown
random
[@0: The tiger eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "bear" "+")
@0: The bear eats the cow.[(triple1)] The bear is blue.[(triple2)] The bear visits the cow.[(triple3)] The cow is big.[(triple4)] The cow visits the lion.[(triple5)] The lion eats the bear.[(triple6)] The tiger visits the bear.[(triple7)] @1: The bear chases the bear.[(((triple3) -> rule3))] @2: The bear chases the tiger.[(((triple1 ((triple3) -> rule3)) -> rule7))] @3: The bear chases the lion.[(((((triple3) -> rule3) ((triple1 ((triple3) -> rule3)) -> rule7)) -> rule5))] @4: The lion chases the cow.[(((triple2 ((((triple3) -> rule3) ((triple1 ((triple3) -> rule3)) -> rule7)) -> rule5)) -> rule8))] @5: The lion is blue.[(((((triple2 ((((triple3) -> rule3) ((triple1 ((triple3) -> rule3)) -> rule7)) -> rule5)) -> rule8)) -> rule2))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear visits the cow.
("bear" "visits" "cow" "+")
triple3
The cow is big.
("cow" "is" "big" "+")
triple4
The cow visits the lion.
("cow" "visits" "lion" "+")
triple5
The lion eats the bear.
("lion" "eats" "bear" "+")
triple6
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple7
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple3) -> (rule3 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
((triple1 ((triple3) -> (rule3 % int2))) -> (rule7 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear chases the lion.
("bear" "chases" "lion" "+")
((((triple3) -> (rule3 % int3)) ((triple1 ((triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear chases the bear.
("bear" "chases" "bear" "+")
int3
The lion chases the cow.
("lion" "chases" "cow" "+")
((triple2 ((((triple3) -> (rule3 % int4)) ((triple1 ((triple3) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The bear chases the lion.
("bear" "chases" "lion" "+")
int2
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int3
The bear chases the bear.
("bear" "chases" "bear" "+")
int4
The lion is blue.
("lion" "is" "blue" "+")
((((triple2 ((((triple3) -> (rule3 % int5)) ((triple1 ((triple3) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The bear chases the lion.
("bear" "chases" "lion" "+")
int3
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int4
The bear chases the bear.
("bear" "chases" "bear" "+")
int5