The dog chases the tiger. The tiger visits the dog. If something chases the tiger and it visits the dog then the tiger visits the dog. If something chases the dog and the dog visits the tiger then the dog does not need the tiger. If something visits the dog then the dog needs the tiger. If something visits the tiger and the tiger is not rough then it needs the dog. If something visits the dog then it does not chase the dog. If something is big then it does not chase the dog. If the dog needs the tiger then the dog is big. If the tiger needs the dog then the tiger is green.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something chases the tiger and it visits the dog then the tiger visits the dog.
((("something" "chases" "tiger" "+") ("something" "visits" "dog" "+")) -> ("tiger" "visits" "dog" "+"))
If something chases the dog and the dog visits the tiger then the dog does not need the tiger.
((("something" "chases" "dog" "+") ("dog" "visits" "tiger" "+")) -> ("dog" "needs" "tiger" "-"))
If something visits the dog then the dog needs the tiger.
((("something" "visits" "dog" "+")) -> ("dog" "needs" "tiger" "+"))
If something visits the tiger and the tiger is not rough then it needs the dog.
((("something" "visits" "tiger" "+") ("tiger" "is" "rough" "~")) -> ("something" "needs" "dog" "+"))
If something visits the dog then it does not chase the dog.
((("something" "visits" "dog" "+")) -> ("something" "chases" "dog" "-"))
If something is big then it does not chase the dog.
((("something" "is" "big" "+")) -> ("something" "chases" "dog" "-"))
If the dog needs the tiger then the dog is big.
((("dog" "needs" "tiger" "+")) -> ("dog" "is" "big" "+"))
If the tiger needs the dog then the tiger is green.
((("tiger" "needs" "dog" "+")) -> ("tiger" "is" "green" "+"))
The tiger visits the dog.
True
1
proof
[(triple2)]
("tiger" "visits" "dog" "+")
triple2
The tiger does not visit the dog.
False
1
inv-proof
[(triple2)]
("tiger" "visits" "dog" "-")
triple2
The tiger does not chase the dog.
True
2
proof
[(((triple2) -> rule5))]
("tiger" "chases" "dog" "-")
((triple2) -> (rule5 % int1))
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
int1
The dog does not need the tiger.
False
2
inv-proof
[(((triple2) -> rule3))]
("dog" "needs" "tiger" "-")
((triple2) -> (rule3 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog is big.
True
3
proof
[(((((triple2) -> rule3)) -> rule7))]
("dog" "is" "big" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int2
The dog is not big.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule7))]
("dog" "is" "big" "-")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int2
The dog does not chase the dog.
True
4
proof
[(((((((triple2) -> rule3)) -> rule7)) -> rule6))]
("dog" "chases" "dog" "-")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int3
The dog chases the dog.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule7)) -> rule6))]
("dog" "chases" "dog" "+")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int3
The tiger is not green.
Unknown
inv-rconc
[@2: The tiger is green.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("tiger" "is" "green" "-")
The tiger needs the dog.
Unknown
rconc
[@1: The tiger needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "needs" "dog" "+")
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "needs" "dog" "-")
The dog visits the tiger.
Unknown
random
[@0: The dog visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "tiger" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The dog chases the tiger.[(triple1)] The tiger visits the dog.[(triple2)] @1: The dog needs the tiger.[(((triple2) -> rule3))] The tiger does not chase the dog.[(((triple2) -> rule5))] @2: The dog is big.[(((((triple2) -> rule3)) -> rule7))] @3: The dog does not chase the dog.[(((((((triple2) -> rule3)) -> rule7)) -> rule6))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
((triple2) -> (rule3 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
((triple2) -> (rule5 % int1))
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
int1
The dog is big.
("dog" "is" "big" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int2
The dog does not chase the dog.
("dog" "chases" "dog" "-")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int3