The rabbit is not rough. The rabbit does not need the tiger. The rabbit visits the tiger. The squirrel does not chase the rabbit. The squirrel chases the tiger. The squirrel is green. The squirrel is not nice. The squirrel does not need the tiger. The tiger chases the squirrel. The tiger visits the rabbit. If something chases the squirrel then the squirrel does not visit the tiger. If something visits the squirrel and the squirrel does not need the tiger then the squirrel does not visit the tiger. If something visits the rabbit then the rabbit does not visit the squirrel. If something needs the tiger and it does not visit the rabbit then it chases the squirrel. If the squirrel does not visit the tiger then the tiger needs the squirrel. All rough things are not blue. If something is rough then it is green. If something needs the squirrel then the squirrel is rough.
The rabbit is not rough.
("rabbit" "is" "rough" "-")
The rabbit does not need the tiger.
("rabbit" "needs" "tiger" "-")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The squirrel does not chase the rabbit.
("squirrel" "chases" "rabbit" "-")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is not nice.
("squirrel" "is" "nice" "-")
The squirrel does not need the tiger.
("squirrel" "needs" "tiger" "-")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If something chases the squirrel then the squirrel does not visit the tiger.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "visits" "tiger" "-"))
If something visits the squirrel and the squirrel does not need the tiger then the squirrel does not visit the tiger.
((("something" "visits" "squirrel" "+") ("squirrel" "needs" "tiger" "~")) -> ("squirrel" "visits" "tiger" "-"))
If something visits the rabbit then the rabbit does not visit the squirrel.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "visits" "squirrel" "-"))
If something needs the tiger and it does not visit the rabbit then it chases the squirrel.
((("something" "needs" "tiger" "+") ("something" "visits" "rabbit" "~")) -> ("something" "chases" "squirrel" "+"))
If the squirrel does not visit the tiger then the tiger needs the squirrel.
((("squirrel" "visits" "tiger" "~")) -> ("tiger" "needs" "squirrel" "+"))
All rough things are not blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "-"))
If something is rough then it is green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something needs the squirrel then the squirrel is rough.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "is" "rough" "+"))
The squirrel is not nice.
True
1
proof
[(triple7)]
("squirrel" "is" "nice" "-")
triple7
The tiger does not chase the squirrel.
False
1
inv-proof
[(triple9)]
("tiger" "chases" "squirrel" "-")
triple9
The rabbit does not visit the squirrel.
True
2
proof
[(((triple10) -> rule3))]
("rabbit" "visits" "squirrel" "-")
((triple10) -> (rule3 % int1))
The rabbit does not visit the squirrel.
("rabbit" "visits" "squirrel" "-")
int1
The rabbit visits the squirrel.
False
2
inv-proof
[(((triple10) -> rule3))]
("rabbit" "visits" "squirrel" "+")
((triple10) -> (rule3 % int1))
The rabbit does not visit the squirrel.
("rabbit" "visits" "squirrel" "-")
int1
The tiger needs the squirrel.
True
3
proof
[(((((triple9) -> rule1)) -> rule5))]
("tiger" "needs" "squirrel" "+")
((((triple9) -> (rule1 % int2))) -> (rule5 % int1))
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int1
The squirrel does not visit the tiger.
("squirrel" "visits" "tiger" "-")
int2
The tiger does not need the squirrel.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule5))]
("tiger" "needs" "squirrel" "-")
((((triple9) -> (rule1 % int2))) -> (rule5 % int1))
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int1
The squirrel does not visit the tiger.
("squirrel" "visits" "tiger" "-")
int2
The squirrel is rough.
True
4
proof
[(((((((triple9) -> rule1)) -> rule5)) -> rule8))]
("squirrel" "is" "rough" "+")
((((((triple9) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int2
The squirrel does not visit the tiger.
("squirrel" "visits" "tiger" "-")
int3
The squirrel is not rough.
False
4
inv-proof
[(((((((triple9) -> rule1)) -> rule5)) -> rule8))]
("squirrel" "is" "rough" "-")
((((((triple9) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int2
The squirrel does not visit the tiger.
("squirrel" "visits" "tiger" "-")
int3
The rabbit is not green.
Unknown
inv-rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "green" "-")
The tiger is green.
Unknown
rconc
[@1: The tiger is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "is" "green" "+")
The squirrel does not chase the squirrel.
Unknown
inv-rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "chases" "squirrel" "-")
The rabbit chases the squirrel.
Unknown
rconc
[@1: The rabbit chases the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "chases" "squirrel" "+")
The rabbit does not chase the tiger.
Unknown
inv-random
[@0: The rabbit chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "tiger" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The tiger visits the squirrel.
Unknown
random
[@0: The tiger visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "squirrel" "+")
@0: The rabbit does not need the tiger.[(triple2)] The rabbit is not rough.[(triple1)] The rabbit visits the tiger.[(triple3)] The squirrel chases the tiger.[(triple5)] The squirrel does not chase the rabbit.[(triple4)] The squirrel does not need the tiger.[(triple8)] The squirrel is green.[(triple6 OR ((((((((triple9) -> rule1)) -> rule5)) -> rule8)) -> rule7))] The squirrel is not nice.[(triple7)] The tiger chases the squirrel.[(triple9)] The tiger visits the rabbit.[(triple10)] @1: The rabbit does not visit the squirrel.[(((triple10) -> rule3))] The squirrel does not visit the tiger.[(((triple9) -> rule1))] @2: The tiger needs the squirrel.[(((((triple9) -> rule1)) -> rule5))] @3: The squirrel is rough.[(((((((triple9) -> rule1)) -> rule5)) -> rule8))] @4: The squirrel is not blue.[(((((((((triple9) -> rule1)) -> rule5)) -> rule8)) -> rule6))]
The rabbit does not need the tiger.
("rabbit" "needs" "tiger" "-")
triple2
The rabbit is not rough.
("rabbit" "is" "rough" "-")
triple1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple3
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple5
The squirrel does not chase the rabbit.
("squirrel" "chases" "rabbit" "-")
triple4
The squirrel does not need the tiger.
("squirrel" "needs" "tiger" "-")
triple8
The squirrel is green.
("squirrel" "is" "green" "+")
triple6
((((((((triple9) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int3
The squirrel does not visit the tiger.
("squirrel" "visits" "tiger" "-")
int4
The squirrel is not nice.
("squirrel" "is" "nice" "-")
triple7
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple9
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple10
The rabbit does not visit the squirrel.
("rabbit" "visits" "squirrel" "-")
((triple10) -> (rule3 % int1))
The rabbit does not visit the squirrel.
("rabbit" "visits" "squirrel" "-")
int1
The squirrel does not visit the tiger.
("squirrel" "visits" "tiger" "-")
((triple9) -> (rule1 % int1))
The squirrel does not visit the tiger.
("squirrel" "visits" "tiger" "-")
int1
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
((((triple9) -> (rule1 % int2))) -> (rule5 % int1))
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int1
The squirrel does not visit the tiger.
("squirrel" "visits" "tiger" "-")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
((((((triple9) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int2
The squirrel does not visit the tiger.
("squirrel" "visits" "tiger" "-")
int3
The squirrel is not blue.
("squirrel" "is" "blue" "-")
((((((((triple9) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel is not blue.
("squirrel" "is" "blue" "-")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int3
The squirrel does not visit the tiger.
("squirrel" "visits" "tiger" "-")
int4