The cat eats the mouse. The cat eats the tiger. The cat is big. The cat is round. The cat is young. The cat sees the tiger. The dog eats the cat. The dog likes the mouse. The dog sees the cat. The mouse is cold. The mouse is green. The mouse sees the cat. The mouse sees the dog. The tiger eats the mouse. The tiger sees the cat. If someone is green then they are cold. If someone is green and they eat the cat then the cat is green. If someone sees the dog then the dog is green. If someone eats the cat and the cat eats the tiger then the tiger is round. If the mouse sees the tiger then the mouse likes the cat. If someone is cold and they see the tiger then the tiger is big.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is green and they eat the cat then the cat is green.
((("someone" "is" "green" "+") ("someone" "eats" "cat" "+")) -> ("cat" "is" "green" "+"))
If someone sees the dog then the dog is green.
((("someone" "sees" "dog" "+")) -> ("dog" "is" "green" "+"))
If someone eats the cat and the cat eats the tiger then the tiger is round.
((("someone" "eats" "cat" "+") ("cat" "eats" "tiger" "+")) -> ("tiger" "is" "round" "+"))
If the mouse sees the tiger then the mouse likes the cat.
((("mouse" "sees" "tiger" "+")) -> ("mouse" "likes" "cat" "+"))
If someone is cold and they see the tiger then the tiger is big.
((("someone" "is" "cold" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "is" "big" "+"))
The cat is round.
True
1
proof
[(triple4)]
("cat" "is" "round" "+")
triple4
The dog does not eat the cat.
False
1
inv-proof
[(triple7)]
("dog" "eats" "cat" "-")
triple7
The dog is green.
True
2
proof
[(((triple13) -> rule3))]
("dog" "is" "green" "+")
((triple13) -> (rule3 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is not green.
False
2
inv-proof
[(((triple13) -> rule3))]
("dog" "is" "green" "-")
((triple13) -> (rule3 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is cold.
True
3
proof
[(((((triple13) -> rule3)) -> rule1))]
("dog" "is" "cold" "+")
((((triple13) -> (rule3 % int2))) -> (rule1 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The cat is not green.
False
4
inv-proof
[(((((triple13) -> rule3) triple7) -> rule2))]
("cat" "is" "green" "-")
((((triple13) -> (rule3 % int2)) triple7) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The cat is cold.
True
5
proof
[(((((((triple13) -> rule3) triple7) -> rule2)) -> rule1))]
("cat" "is" "cold" "+")
((((((triple13) -> (rule3 % int3)) triple7) -> (rule2 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The dog is green.
("dog" "is" "green" "+")
int3
The cat is not cold.
False
5
inv-proof
[(((((((triple13) -> rule3) triple7) -> rule2)) -> rule1))]
("cat" "is" "cold" "-")
((((((triple13) -> (rule3 % int3)) triple7) -> (rule2 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The dog is green.
("dog" "is" "green" "+")
int3
The mouse does not like the cat.
Unknown
inv-rconc
[@1: The mouse likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "likes" "cat" "-")
The tiger is cold.
Unknown
rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "cold" "+")
The tiger does not see the dog.
Unknown
inv-random
[@0: The tiger sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "dog" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The mouse does not see the tiger.
Unknown
inv-random
[@0: The mouse sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "tiger" "-")
The dog sees the mouse.
Unknown
random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "+")
The cat does not like the dog.
Unknown
inv-random
[@0: The cat likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "dog" "-")
The tiger likes the dog.
Unknown
random
[@0: The tiger likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "dog" "+")
@0: The cat eats the mouse.[(triple1)] The cat eats the tiger.[(triple2)] The cat is big.[(triple3)] The cat is round.[(triple4)] The cat is young.[(triple5)] The cat sees the tiger.[(triple6)] The dog eats the cat.[(triple7)] The dog likes the mouse.[(triple8)] The dog sees the cat.[(triple9)] The mouse is cold.[(triple10 OR ((triple11) -> rule1))] The mouse is green.[(triple11)] The mouse sees the cat.[(triple12)] The mouse sees the dog.[(triple13)] The tiger eats the mouse.[(triple14)] The tiger sees the cat.[(triple15)] @1: The dog is green.[(((triple13) -> rule3))] The tiger is round.[(((triple7 triple2) -> rule4))] @2: The cat is green.[(((((triple13) -> rule3) triple7) -> rule2))] The dog is cold.[(((((triple13) -> rule3)) -> rule1))] @3: The cat is cold.[(((((((triple13) -> rule3) triple7) -> rule2)) -> rule1))] @4: The tiger is big.[(((((((((triple13) -> rule3) triple7) -> rule2)) -> rule1) triple6) -> rule6))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple2
The cat is big.
("cat" "is" "big" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple6
The dog eats the cat.
("dog" "eats" "cat" "+")
triple7
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple8
The dog sees the cat.
("dog" "sees" "cat" "+")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
((triple11) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
triple11
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple12
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple13
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple14
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple15
The dog is green.
("dog" "is" "green" "+")
((triple13) -> (rule3 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((triple7 triple2) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The cat is green.
("cat" "is" "green" "+")
((((triple13) -> (rule3 % int2)) triple7) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
((((triple13) -> (rule3 % int2))) -> (rule1 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
((((((triple13) -> (rule3 % int3)) triple7) -> (rule2 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The dog is green.
("dog" "is" "green" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
((((((((triple13) -> (rule3 % int4)) triple7) -> (rule2 % int3))) -> (rule1 % int2)) triple6) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
The dog is green.
("dog" "is" "green" "+")
int4