The dog is green. The dog does not see the squirrel. The dog visits the squirrel. The rabbit visits the squirrel. The squirrel eats the tiger. The tiger sees the rabbit. The tiger sees the squirrel. If something is green and it does not eat the dog then it does not visit the squirrel. If something visits the tiger and it does not see the tiger then it is blue. If the rabbit is green then the rabbit eats the squirrel. If the rabbit eats the dog then the dog visits the rabbit. If something eats the rabbit then the rabbit is green. If something is round then it eats the rabbit. Green things are round. If something visits the rabbit and the rabbit eats the dog then it visits the dog.
The dog is green.
("dog" "is" "green" "+")
The dog does not see the squirrel.
("dog" "sees" "squirrel" "-")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If something is green and it does not eat the dog then it does not visit the squirrel.
((("something" "is" "green" "+") ("something" "eats" "dog" "~")) -> ("something" "visits" "squirrel" "-"))
If something visits the tiger and it does not see the tiger then it is blue.
((("something" "visits" "tiger" "+") ("something" "sees" "tiger" "~")) -> ("something" "is" "blue" "+"))
If the rabbit is green then the rabbit eats the squirrel.
((("rabbit" "is" "green" "+")) -> ("rabbit" "eats" "squirrel" "+"))
If the rabbit eats the dog then the dog visits the rabbit.
((("rabbit" "eats" "dog" "+")) -> ("dog" "visits" "rabbit" "+"))
If something eats the rabbit then the rabbit is green.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If something is round then it eats the rabbit.
((("something" "is" "round" "+")) -> ("something" "eats" "rabbit" "+"))
Green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something visits the rabbit and the rabbit eats the dog then it visits the dog.
((("something" "visits" "rabbit" "+") ("rabbit" "eats" "dog" "+")) -> ("something" "visits" "dog" "+"))
The dog visits the squirrel.
True
1
proof
[(triple3)]
("dog" "visits" "squirrel" "+")
triple3
The tiger does not see the rabbit.
False
1
inv-proof
[(triple6)]
("tiger" "sees" "rabbit" "-")
triple6
The dog is round.
True
2
proof
[(((triple1) -> rule7))]
("dog" "is" "round" "+")
((triple1) -> (rule7 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is not round.
False
2
inv-proof
[(((triple1) -> rule7))]
("dog" "is" "round" "-")
((triple1) -> (rule7 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog eats the rabbit.
True
3
proof
[(((((triple1) -> rule7)) -> rule6))]
("dog" "eats" "rabbit" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog does not eat the rabbit.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule6))]
("dog" "eats" "rabbit" "-")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The rabbit is green.
True
4
proof
[(((((((triple1) -> rule7)) -> rule6)) -> rule5))]
("rabbit" "is" "green" "+")
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3
The rabbit is not green.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule6)) -> rule5))]
("rabbit" "is" "green" "-")
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3
The rabbit is round.
True
5
proof
[(((((((((triple1) -> rule7)) -> rule6)) -> rule5)) -> rule7))]
("rabbit" "is" "round" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The dog is round.
("dog" "is" "round" "+")
int4
The rabbit is not round.
False
5
inv-proof
[(((((((((triple1) -> rule7)) -> rule6)) -> rule5)) -> rule7))]
("rabbit" "is" "round" "-")
((((((((triple1) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The dog is round.
("dog" "is" "round" "+")
int4
The rabbit eats the rabbit.
True
6
proof
[(((((((((((triple1) -> rule7)) -> rule6)) -> rule5)) -> rule7)) -> rule6))]
("rabbit" "eats" "rabbit" "+")
((((((((((triple1) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int4
The dog is round.
("dog" "is" "round" "+")
int5
The rabbit does not eat the rabbit.
False
6
inv-proof
[(((((((((((triple1) -> rule7)) -> rule6)) -> rule5)) -> rule7)) -> rule6))]
("rabbit" "eats" "rabbit" "-")
((((((((((triple1) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int4
The dog is round.
("dog" "is" "round" "+")
int5
The squirrel does not visit the dog.
Unknown
inv-rconc
[@1: The squirrel visits the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "visits" "dog" "-")
The dog is blue.
Unknown
rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "blue" "+")
The squirrel is not blue.
Unknown
inv-rconc
[@1: The squirrel is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "blue" "-")
The tiger is blue.
Unknown
rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "blue" "+")
The tiger does not eat the rabbit.
Unknown
inv-rconc
[@2: The tiger eats the rabbit.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("tiger" "eats" "rabbit" "-")
The rabbit visits the dog.
Unknown
rconc
[@1: The rabbit visits the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "visits" "dog" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The rabbit does not see the tiger.
Unknown
inv-random
[@0: The rabbit sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "tiger" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The dog does not see the squirrel.[(triple2)] The dog is green.[(triple1)] The dog visits the squirrel.[(triple3)] The rabbit visits the squirrel.[(triple4)] The squirrel eats the tiger.[(triple5)] The tiger sees the rabbit.[(triple6)] The tiger sees the squirrel.[(triple7)] @1: The dog is round.[(((triple1) -> rule7))] @2: The dog eats the rabbit.[(((((triple1) -> rule7)) -> rule6))] @3: The rabbit is green.[(((((((triple1) -> rule7)) -> rule6)) -> rule5))] @4: The rabbit eats the squirrel.[(((((((((triple1) -> rule7)) -> rule6)) -> rule5)) -> rule3))] The rabbit is round.[(((((((((triple1) -> rule7)) -> rule6)) -> rule5)) -> rule7))] @5: The rabbit eats the rabbit.[(((((((((((triple1) -> rule7)) -> rule6)) -> rule5)) -> rule7)) -> rule6))]
The dog does not see the squirrel.
("dog" "sees" "squirrel" "-")
triple2
The dog is green.
("dog" "is" "green" "+")
triple1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple3
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple4
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple5
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple6
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple7
The dog is round.
("dog" "is" "round" "+")
((triple1) -> (rule7 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The dog is round.
("dog" "is" "round" "+")
int4
The rabbit is round.
("rabbit" "is" "round" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The dog is round.
("dog" "is" "round" "+")
int4
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((((((((triple1) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int4
The dog is round.
("dog" "is" "round" "+")
int5