The dog chases the lion. The dog eats the lion. The dog is kind. The dog is not round. The dog visits the lion. The lion does not chase the dog. The lion is not nice. If the dog chases the lion and the dog is kind then the dog visits the lion. If someone is green and they chase the dog then they visit the lion. If someone is kind then they eat the dog. If someone is kind then they visit the dog. If someone chases the dog and the dog is not green then they eat the lion. If someone eats the dog then they chase the dog. If the lion visits the dog then the lion is round. If someone chases the dog and they chase the lion then the dog is not nice.
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is not round.
("dog" "is" "round" "-")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion does not chase the dog.
("lion" "chases" "dog" "-")
The lion is not nice.
("lion" "is" "nice" "-")
If the dog chases the lion and the dog is kind then the dog visits the lion.
((("dog" "chases" "lion" "+") ("dog" "is" "kind" "+")) -> ("dog" "visits" "lion" "+"))
If someone is green and they chase the dog then they visit the lion.
((("someone" "is" "green" "+") ("someone" "chases" "dog" "+")) -> ("someone" "visits" "lion" "+"))
If someone is kind then they eat the dog.
((("someone" "is" "kind" "+")) -> ("someone" "eats" "dog" "+"))
If someone is kind then they visit the dog.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "dog" "+"))
If someone chases the dog and the dog is not green then they eat the lion.
((("someone" "chases" "dog" "+") ("dog" "is" "green" "~")) -> ("someone" "eats" "lion" "+"))
If someone eats the dog then they chase the dog.
((("someone" "eats" "dog" "+")) -> ("someone" "chases" "dog" "+"))
If the lion visits the dog then the lion is round.
((("lion" "visits" "dog" "+")) -> ("lion" "is" "round" "+"))
If someone chases the dog and they chase the lion then the dog is not nice.
((("someone" "chases" "dog" "+") ("someone" "chases" "lion" "+")) -> ("dog" "is" "nice" "-"))
The lion does not chase the dog.
True
1
proof
[(triple6)]
("lion" "chases" "dog" "-")
triple6
The lion chases the dog.
False
1
inv-proof
[(triple6)]
("lion" "chases" "dog" "+")
triple6
The dog visits the dog.
True
2
proof
[(((triple3) -> rule4))]
("dog" "visits" "dog" "+")
((triple3) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog does not eat the dog.
False
2
inv-proof
[(((triple3) -> rule3))]
("dog" "eats" "dog" "-")
((triple3) -> (rule3 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog chases the dog.
True
3
proof
[(((((triple3) -> rule3)) -> rule6))]
("dog" "chases" "dog" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog does not chase the dog.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule6))]
("dog" "chases" "dog" "-")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog is not nice.
True
5
proof
[(((((((triple3) -> rule3)) -> rule6) triple1) -> rule8))]
("dog" "is" "nice" "-")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2)) triple1) -> (rule8 % int1))
The dog is not nice.
("dog" "is" "nice" "-")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
int3
The dog is nice.
False
5
inv-proof
[(((((((triple3) -> rule3)) -> rule6) triple1) -> rule8))]
("dog" "is" "nice" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2)) triple1) -> (rule8 % int1))
The dog is not nice.
("dog" "is" "nice" "-")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
int3
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "lion" "-")
The lion eats the lion.
Unknown
rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "eats" "lion" "+")
The lion is not round.
Unknown
inv-rconc
[@2: The lion is round.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("lion" "is" "round" "-")
The lion eats the dog.
Unknown
rconc
[@1: The lion eats the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "eats" "dog" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
The lion is not blue.
Unknown
inv-random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
@0: The dog chases the lion.[(triple1)] The dog eats the lion.[(triple2)] The dog is kind.[(triple3)] The dog is not round.[(triple4)] The dog visits the lion.[(triple5 OR ((triple1 triple3) -> rule1))] The lion does not chase the dog.[(triple6)] The lion is not nice.[(triple7)] @1: The dog eats the dog.[(((triple3) -> rule3))] The dog visits the dog.[(((triple3) -> rule4))] @2: The dog chases the dog.[(((((triple3) -> rule3)) -> rule6))] @3: The dog is not nice.[(((((((triple3) -> rule3)) -> rule6) triple1) -> rule8))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
The dog eats the lion.
("dog" "eats" "lion" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog is not round.
("dog" "is" "round" "-")
triple4
The dog visits the lion.
("dog" "visits" "lion" "+")
triple5
((triple1 triple3) -> (rule1 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The lion does not chase the dog.
("lion" "chases" "dog" "-")
triple6
The lion is not nice.
("lion" "is" "nice" "-")
triple7
The dog eats the dog.
("dog" "eats" "dog" "+")
((triple3) -> (rule3 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple3) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog is not nice.
("dog" "is" "nice" "-")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2)) triple1) -> (rule8 % int1))
The dog is not nice.
("dog" "is" "nice" "-")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
int3