The cat needs the dog. The cat does not see the dog. The dog is green. The dog is rough. The dog is round. The dog needs the cat. The dog visits the cat. If someone is green and they visit the dog then they see the cat. If someone needs the dog and they do not need the cat then the cat is not rough. If the cat is rough then the cat does not need the dog. If someone sees the cat then the cat is green. If someone visits the dog then they need the dog. If someone sees the dog then the dog visits the cat. If someone is rough then they visit the dog. If someone is nice and they do not visit the dog then they are red.
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat does not see the dog.
("cat" "sees" "dog" "-")
The dog is green.
("dog" "is" "green" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
If someone is green and they visit the dog then they see the cat.
((("someone" "is" "green" "+") ("someone" "visits" "dog" "+")) -> ("someone" "sees" "cat" "+"))
If someone needs the dog and they do not need the cat then the cat is not rough.
((("someone" "needs" "dog" "+") ("someone" "needs" "cat" "~")) -> ("cat" "is" "rough" "-"))
If the cat is rough then the cat does not need the dog.
((("cat" "is" "rough" "+")) -> ("cat" "needs" "dog" "-"))
If someone sees the cat then the cat is green.
((("someone" "sees" "cat" "+")) -> ("cat" "is" "green" "+"))
If someone visits the dog then they need the dog.
((("someone" "visits" "dog" "+")) -> ("someone" "needs" "dog" "+"))
If someone sees the dog then the dog visits the cat.
((("someone" "sees" "dog" "+")) -> ("dog" "visits" "cat" "+"))
If someone is rough then they visit the dog.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "dog" "+"))
If someone is nice and they do not visit the dog then they are red.
((("someone" "is" "nice" "+") ("someone" "visits" "dog" "~")) -> ("someone" "is" "red" "+"))
The dog needs the cat.
True
1
proof
[(triple6)]
("dog" "needs" "cat" "+")
triple6
The dog does not need the cat.
False
1
inv-proof
[(triple6)]
("dog" "needs" "cat" "-")
triple6
The dog visits the dog.
True
2
proof
[(((triple4) -> rule7))]
("dog" "visits" "dog" "+")
((triple4) -> (rule7 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog does not visit the dog.
False
2
inv-proof
[(((triple4) -> rule7))]
("dog" "visits" "dog" "-")
((triple4) -> (rule7 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog needs the dog.
True
3
proof
[(((((triple4) -> rule7)) -> rule5))]
("dog" "needs" "dog" "+")
((((triple4) -> (rule7 % int2))) -> (rule5 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog does not see the cat.
False
4
inv-proof
[(((triple3 ((triple4) -> rule7)) -> rule1))]
("dog" "sees" "cat" "-")
((triple3 ((triple4) -> (rule7 % int2))) -> (rule1 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The cat is green.
True
5
proof
[(((((triple3 ((triple4) -> rule7)) -> rule1)) -> rule4))]
("cat" "is" "green" "+")
((((triple3 ((triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The cat is not green.
False
5
inv-proof
[(((((triple3 ((triple4) -> rule7)) -> rule1)) -> rule4))]
("cat" "is" "green" "-")
((((triple3 ((triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The cat does not visit the dog.
Unknown
inv-rconc
[@1: The cat visits the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "visits" "dog" "-")
The cat is red.
Unknown
rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "red" "+")
The dog is not red.
Unknown
inv-rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "is" "red" "-")
The cat sees the cat.
Unknown
rconc
[@2: The cat sees the cat.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("cat" "sees" "cat" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
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 cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The cat does not see the dog.[(triple2)] The cat needs the dog.[(triple1)] The dog is green.[(triple3)] The dog is rough.[(triple4)] The dog is round.[(triple5)] The dog needs the cat.[(triple6)] The dog visits the cat.[(triple7)] @1: The dog visits the dog.[(((triple4) -> rule7))] @2: The dog needs the dog.[(((((triple4) -> rule7)) -> rule5))] The dog sees the cat.[(((triple3 ((triple4) -> rule7)) -> rule1))] @3: The cat is green.[(((((triple3 ((triple4) -> rule7)) -> rule1)) -> rule4))]
The cat does not see the dog.
("cat" "sees" "dog" "-")
triple2
The cat needs the dog.
("cat" "needs" "dog" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple5
The dog needs the cat.
("dog" "needs" "cat" "+")
triple6
The dog visits the cat.
("dog" "visits" "cat" "+")
triple7
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple4) -> (rule7 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
((((triple4) -> (rule7 % int2))) -> (rule5 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog sees the cat.
("dog" "sees" "cat" "+")
((triple3 ((triple4) -> (rule7 % int2))) -> (rule1 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The cat is green.
("cat" "is" "green" "+")
((((triple3 ((triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3