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