The bear eats the cat. The cat is nice. The rabbit eats the cat. The tiger eats the cat. If something eats the rabbit then it is rough. If something chases the tiger and it sees the rabbit then the rabbit is blue. If something is cold and it sees the cat then the cat eats the rabbit. If something eats the cat then the cat sees the tiger. If something chases the rabbit then it eats the rabbit. If something sees the tiger then the tiger chases the rabbit. If something sees the cat and the cat eats the bear then it is big. If the rabbit sees the cat and the cat sees the bear then the cat chases the tiger.
The bear eats the cat.
("bear" "eats" "cat" "+")
The cat is nice.
("cat" "is" "nice" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
If something eats the rabbit then it is rough.
((("something" "eats" "rabbit" "+")) -> ("something" "is" "rough" "+"))
If something chases the tiger and it sees the rabbit then the rabbit is blue.
((("something" "chases" "tiger" "+") ("something" "sees" "rabbit" "+")) -> ("rabbit" "is" "blue" "+"))
If something is cold and it sees the cat then the cat eats the rabbit.
((("something" "is" "cold" "+") ("something" "sees" "cat" "+")) -> ("cat" "eats" "rabbit" "+"))
If something eats the cat then the cat sees the tiger.
((("something" "eats" "cat" "+")) -> ("cat" "sees" "tiger" "+"))
If something chases the rabbit then it eats the rabbit.
((("something" "chases" "rabbit" "+")) -> ("something" "eats" "rabbit" "+"))
If something sees the tiger then the tiger chases the rabbit.
((("something" "sees" "tiger" "+")) -> ("tiger" "chases" "rabbit" "+"))
If something sees the cat and the cat eats the bear then it is big.
((("something" "sees" "cat" "+") ("cat" "eats" "bear" "+")) -> ("something" "is" "big" "+"))
If the rabbit sees the cat and the cat sees the bear then the cat chases the tiger.
((("rabbit" "sees" "cat" "+") ("cat" "sees" "bear" "+")) -> ("cat" "chases" "tiger" "+"))
The cat is nice.
True
1
proof
[(triple2)]
("cat" "is" "nice" "+")
triple2
The rabbit does not eat the cat.
False
1
inv-proof
[(triple3)]
("rabbit" "eats" "cat" "-")
triple3
The cat sees the tiger.
True
2
proof
[(((triple1) -> rule4) OR ((triple3) -> rule4) OR ((triple4) -> rule4))]
("cat" "sees" "tiger" "+")
((triple1) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((triple3) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((triple4) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat does not see the tiger.
False
2
inv-proof
[(((triple1) -> rule4) OR ((triple3) -> rule4) OR ((triple4) -> rule4))]
("cat" "sees" "tiger" "-")
((triple1) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((triple3) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((triple4) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The tiger chases the rabbit.
True
3
proof
[(((((triple1) -> rule4)) -> rule6) OR ((((triple3) -> rule4)) -> rule6) OR ((((triple4) -> rule4)) -> rule6))]
("tiger" "chases" "rabbit" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The tiger does not chase the rabbit.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6) OR ((((triple3) -> rule4)) -> rule6) OR ((((triple4) -> rule4)) -> rule6))]
("tiger" "chases" "rabbit" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The tiger eats the rabbit.
True
4
proof
[(((((((triple1) -> rule4)) -> rule6)) -> rule5) OR ((((((triple3) -> rule4)) -> rule6)) -> rule5) OR ((((((triple4) -> rule4)) -> rule6)) -> rule5))]
("tiger" "eats" "rabbit" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The tiger does not eat the rabbit.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule6)) -> rule5) OR ((((((triple3) -> rule4)) -> rule6)) -> rule5) OR ((((((triple4) -> rule4)) -> rule6)) -> rule5))]
("tiger" "eats" "rabbit" "-")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The bear does not eat the rabbit.
Unknown
inv-rconc
[@1: The bear eats the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "rabbit" "-")
The cat is rough.
Unknown
rconc
[@2: The cat is rough.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("cat" "is" "rough" "+")
The cat does not eat the rabbit.
Unknown
inv-rconc
[@1: The cat eats the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "eats" "rabbit" "-")
The rabbit is rough.
Unknown
rconc
[@2: The rabbit is rough.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("rabbit" "is" "rough" "+")
The tiger does not eat the bear.
Unknown
inv-random
[@0: The tiger eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "bear" "-")
The rabbit sees the cat.
Unknown
random
[@0: The rabbit sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "cat" "+")
The tiger is not blue.
Unknown
inv-random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "-")
The rabbit sees the tiger.
Unknown
random
[@0: The rabbit sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "tiger" "+")
@0: The bear eats the cat.[(triple1)] The cat is nice.[(triple2)] The rabbit eats the cat.[(triple3)] The tiger eats the cat.[(triple4)] @1: The cat sees the tiger.[(((triple1) -> rule4) OR ((triple3) -> rule4) OR ((triple4) -> rule4))] @2: The tiger chases the rabbit.[(((((triple1) -> rule4)) -> rule6) OR ((((triple3) -> rule4)) -> rule6) OR ((((triple4) -> rule4)) -> rule6))] @3: The tiger eats the rabbit.[(((((((triple1) -> rule4)) -> rule6)) -> rule5) OR ((((((triple3) -> rule4)) -> rule6)) -> rule5) OR ((((((triple4) -> rule4)) -> rule6)) -> rule5))] @4: The tiger is rough.[(((((((((triple1) -> rule4)) -> rule6)) -> rule5)) -> rule1) OR ((((((((triple3) -> rule4)) -> rule6)) -> rule5)) -> rule1) OR ((((((((triple4) -> rule4)) -> rule6)) -> rule5)) -> rule1))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple3
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple4
The cat sees the tiger.
("cat" "sees" "tiger" "+")
((triple1) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((triple3) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((triple4) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
((((((((triple1) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int4
((((((((triple3) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int4
((((((((triple4) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int4