The cat eats the dog. The dog is green. If someone is round and they see the dog then they need the cat. If someone eats the cat and they need the cat then they are cold. If someone eats the dog and they are big then the dog needs the cat. If someone eats the dog then the dog is round. If someone sees the dog and the dog needs the cat then they eat the dog. If someone needs the cat then they are cold. If someone sees the cat and they are big then they need the dog. If someone is round then they need the cat.
The cat eats the dog.
("cat" "eats" "dog" "+")
The dog is green.
("dog" "is" "green" "+")
If someone is round and they see the dog then they need the cat.
((("someone" "is" "round" "+") ("someone" "sees" "dog" "+")) -> ("someone" "needs" "cat" "+"))
If someone eats the cat and they need the cat then they are cold.
((("someone" "eats" "cat" "+") ("someone" "needs" "cat" "+")) -> ("someone" "is" "cold" "+"))
If someone eats the dog and they are big then the dog needs the cat.
((("someone" "eats" "dog" "+") ("someone" "is" "big" "+")) -> ("dog" "needs" "cat" "+"))
If someone eats the dog then the dog is round.
((("someone" "eats" "dog" "+")) -> ("dog" "is" "round" "+"))
If someone sees the dog and the dog needs the cat then they eat the dog.
((("someone" "sees" "dog" "+") ("dog" "needs" "cat" "+")) -> ("someone" "eats" "dog" "+"))
If someone needs the cat then they are cold.
((("someone" "needs" "cat" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the cat and they are big then they need the dog.
((("someone" "sees" "cat" "+") ("someone" "is" "big" "+")) -> ("someone" "needs" "dog" "+"))
If someone is round then they need the cat.
((("someone" "is" "round" "+")) -> ("someone" "needs" "cat" "+"))
The dog is green.
True
1
proof
[(triple2)]
("dog" "is" "green" "+")
triple2
The dog is not green.
False
1
inv-proof
[(triple2)]
("dog" "is" "green" "-")
triple2
The dog is round.
True
2
proof
[(((triple1) -> rule4))]
("dog" "is" "round" "+")
((triple1) -> (rule4 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is not round.
False
2
inv-proof
[(((triple1) -> rule4))]
("dog" "is" "round" "-")
((triple1) -> (rule4 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog needs the cat.
True
3
proof
[(((((triple1) -> rule4)) -> rule8))]
("dog" "needs" "cat" "+")
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog does not need the cat.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule8))]
("dog" "needs" "cat" "-")
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is cold.
True
4
proof
[(((((((triple1) -> rule4)) -> rule8)) -> rule6))]
("dog" "is" "cold" "+")
((((((triple1) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3
The dog is not cold.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule8)) -> rule6))]
("dog" "is" "cold" "-")
((((((triple1) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "cat" "-")
The cat is cold.
Unknown
rconc
[@2: The cat is cold.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("cat" "is" "cold" "+")
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "eats" "dog" "-")
The cat needs the dog.
Unknown
rconc
[@1: The cat needs the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "needs" "dog" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The dog sees the cat.
Unknown
random
[@0: The dog sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cat" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
@0: The cat eats the dog.[(triple1)] The dog is green.[(triple2)] @1: The dog is round.[(((triple1) -> rule4))] @2: The dog needs the cat.[(((((triple1) -> rule4)) -> rule8))] @3: The dog is cold.[(((((((triple1) -> rule4)) -> rule8)) -> rule6))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is round.
("dog" "is" "round" "+")
((triple1) -> (rule4 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
((((((triple1) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3