The cow is cold. The cow is red. The cow visits the tiger. The lion chases the tiger. The lion is rough. The lion is round. The lion sees the cow. The lion sees the squirrel. The squirrel is cold. The squirrel visits the tiger. The tiger chases the lion. The tiger is red. If something is cold and blue then it chases the cow. If something sees the tiger then the tiger is round. If something is blue then it is red. If something chases the tiger and the tiger sees the cow then the cow sees the tiger. If something is round and it sees the cow then the cow visits the tiger. If something chases the cow then the cow chases the tiger. If the squirrel chases the tiger and the tiger is round then the squirrel visits the cow. If something sees the squirrel then it is blue. Rough, red things are cold.
The cow is cold.
("cow" "is" "cold" "+")
The cow is red.
("cow" "is" "red" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger is red.
("tiger" "is" "red" "+")
If something is cold and blue then it chases the cow.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "chases" "cow" "+"))
If something sees the tiger then the tiger is round.
((("something" "sees" "tiger" "+")) -> ("tiger" "is" "round" "+"))
If something is blue then it is red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something chases the tiger and the tiger sees the cow then the cow sees the tiger.
((("something" "chases" "tiger" "+") ("tiger" "sees" "cow" "+")) -> ("cow" "sees" "tiger" "+"))
If something is round and it sees the cow then the cow visits the tiger.
((("something" "is" "round" "+") ("something" "sees" "cow" "+")) -> ("cow" "visits" "tiger" "+"))
If something chases the cow then the cow chases the tiger.
((("something" "chases" "cow" "+")) -> ("cow" "chases" "tiger" "+"))
If the squirrel chases the tiger and the tiger is round then the squirrel visits the cow.
((("squirrel" "chases" "tiger" "+") ("tiger" "is" "round" "+")) -> ("squirrel" "visits" "cow" "+"))
If something sees the squirrel then it is blue.
((("something" "sees" "squirrel" "+")) -> ("something" "is" "blue" "+"))
Rough, red things are cold.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
The cow is cold.
True
1
proof
[(triple1)]
("cow" "is" "cold" "+")
triple1
The lion is not round.
False
1
inv-proof
[(triple6)]
("lion" "is" "round" "-")
triple6
The lion is blue.
True
2
proof
[(((triple8) -> rule8))]
("lion" "is" "blue" "+")
((triple8) -> (rule8 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is not blue.
False
2
inv-proof
[(((triple8) -> rule8))]
("lion" "is" "blue" "-")
((triple8) -> (rule8 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is red.
True
3
proof
[(((((triple8) -> rule8)) -> rule3))]
("lion" "is" "red" "+")
((((triple8) -> (rule8 % int2))) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is not red.
False
3
inv-proof
[(((((triple8) -> rule8)) -> rule3))]
("lion" "is" "red" "-")
((((triple8) -> (rule8 % int2))) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is cold.
True
5
proof
[(((triple5 ((((triple8) -> rule8)) -> rule3)) -> rule9))]
("lion" "is" "cold" "+")
((triple5 ((((triple8) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion is not cold.
False
5
inv-proof
[(((triple5 ((((triple8) -> rule8)) -> rule3)) -> rule9))]
("lion" "is" "cold" "-")
((triple5 ((((triple8) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion chases the cow.
True
8
proof
[(((((triple5 ((((triple8) -> rule8)) -> rule3)) -> rule9) ((triple8) -> rule8)) -> rule1))]
("lion" "chases" "cow" "+")
((((triple5 ((((triple8) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule9 % int2)) ((triple8) -> (rule8 % int4))) -> (rule1 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The lion is blue.
("lion" "is" "blue" "+")
int4
The lion does not chase the cow.
False
8
inv-proof
[(((((triple5 ((((triple8) -> rule8)) -> rule3)) -> rule9) ((triple8) -> rule8)) -> rule1))]
("lion" "chases" "cow" "-")
((((triple5 ((((triple8) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule9 % int2)) ((triple8) -> (rule8 % int4))) -> (rule1 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The lion is blue.
("lion" "is" "blue" "+")
int4
The cow chases the tiger.
True
9
proof
[(((((((triple5 ((((triple8) -> rule8)) -> rule3)) -> rule9) ((triple8) -> rule8)) -> rule1)) -> rule6))]
("cow" "chases" "tiger" "+")
((((((triple5 ((((triple8) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule9 % int3)) ((triple8) -> (rule8 % int5))) -> (rule1 % int2))) -> (rule6 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The lion is blue.
("lion" "is" "blue" "+")
int5
The cow does not chase the tiger.
False
9
inv-proof
[(((((((triple5 ((((triple8) -> rule8)) -> rule3)) -> rule9) ((triple8) -> rule8)) -> rule1)) -> rule6))]
("cow" "chases" "tiger" "-")
((((((triple5 ((((triple8) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule9 % int3)) ((triple8) -> (rule8 % int5))) -> (rule1 % int2))) -> (rule6 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The lion is blue.
("lion" "is" "blue" "+")
int5
The squirrel is not blue.
Unknown
inv-rconc
[@1: The squirrel is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "is" "blue" "-")
The cow chases the cow.
Unknown
rconc
[@2: The cow chases the cow.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("cow" "chases" "cow" "+")
The tiger does not chase the cow.
Unknown
inv-rconc
[@2: The tiger chases the cow.[CWA. Example of deepest failure = (rule1 <- rule9 <- FAIL)]]
("tiger" "chases" "cow" "-")
The squirrel visits the cow.
Unknown
rconc
[@1: The squirrel visits the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "visits" "cow" "+")
The tiger is not cold.
Unknown
inv-rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("tiger" "is" "cold" "-")
The squirrel chases the cow.
Unknown
rconc
[@2: The squirrel chases the cow.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("squirrel" "chases" "cow" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel sees the cow.
Unknown
random
[@0: The squirrel sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "cow" "+")
The cow does not visit the squirrel.
Unknown
inv-random
[@0: The cow visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "squirrel" "-")
The squirrel sees the tiger.
Unknown
random
[@0: The squirrel sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "tiger" "+")
The lion does not chase the squirrel.
Unknown
inv-random
[@0: The lion chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "squirrel" "-")
The squirrel chases the tiger.
Unknown
random
[@0: The squirrel chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "tiger" "+")
@0: The cow is cold.[(triple1)] The cow is red.[(triple2)] The cow visits the tiger.[(triple3 OR ((triple6 triple7) -> rule5))] The lion chases the tiger.[(triple4)] The lion is rough.[(triple5)] The lion is round.[(triple6)] The lion sees the cow.[(triple7)] The lion sees the squirrel.[(triple8)] The squirrel is cold.[(triple9)] The squirrel visits the tiger.[(triple10)] The tiger chases the lion.[(triple11)] The tiger is red.[(triple12)] @1: The lion is blue.[(((triple8) -> rule8))] @2: The lion is red.[(((((triple8) -> rule8)) -> rule3))] @3: The lion is cold.[(((triple5 ((((triple8) -> rule8)) -> rule3)) -> rule9))] @4: The lion chases the cow.[(((((triple5 ((((triple8) -> rule8)) -> rule3)) -> rule9) ((triple8) -> rule8)) -> rule1))] @5: The cow chases the tiger.[(((((((triple5 ((((triple8) -> rule8)) -> rule3)) -> rule9) ((triple8) -> rule8)) -> rule1)) -> rule6))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple3
((triple6 triple7) -> (rule5 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
The lion is round.
("lion" "is" "round" "+")
triple6
The lion sees the cow.
("lion" "sees" "cow" "+")
triple7
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple8
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple10
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple11
The tiger is red.
("tiger" "is" "red" "+")
triple12
The lion is blue.
("lion" "is" "blue" "+")
((triple8) -> (rule8 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is red.
("lion" "is" "red" "+")
((((triple8) -> (rule8 % int2))) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
((triple5 ((((triple8) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion chases the cow.
("lion" "chases" "cow" "+")
((((triple5 ((((triple8) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule9 % int2)) ((triple8) -> (rule8 % int4))) -> (rule1 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The lion is blue.
("lion" "is" "blue" "+")
int4
The cow chases the tiger.
("cow" "chases" "tiger" "+")
((((((triple5 ((((triple8) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule9 % int3)) ((triple8) -> (rule8 % int5))) -> (rule1 % int2))) -> (rule6 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The lion is blue.
("lion" "is" "blue" "+")
int5