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