The cat is big. The cat is kind. The cat does not need the dog. The cat needs the lion. The cat sees the lion. The cat visits the dog. The dog is big. The dog needs the lion. The dog visits the cat. The dog visits the lion. The lion is not rough. The lion is round. The lion needs the cat. The lion needs the dog. The lion does not visit the cat. If someone visits the cat then they need the dog. If the cat is kind and the cat does not need the lion then the lion is cold. If someone is big then they see the dog. If someone needs the lion and they see the lion then the lion is kind. If someone sees the dog then the dog is not round. If someone needs the cat and they do not see the dog then they visit the dog. If someone sees the cat then they visit the dog. If the lion visits the dog then the lion sees the cat.
The cat is big.
("cat" "is" "big" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat does not need the dog.
("cat" "needs" "dog" "-")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog is big.
("dog" "is" "big" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion is not rough.
("lion" "is" "rough" "-")
The lion is round.
("lion" "is" "round" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion does not visit the cat.
("lion" "visits" "cat" "-")
If someone visits the cat then they need the dog.
((("someone" "visits" "cat" "+")) -> ("someone" "needs" "dog" "+"))
If the cat is kind and the cat does not need the lion then the lion is cold.
((("cat" "is" "kind" "+") ("cat" "needs" "lion" "~")) -> ("lion" "is" "cold" "+"))
If someone is big then they see the dog.
((("someone" "is" "big" "+")) -> ("someone" "sees" "dog" "+"))
If someone needs the lion and they see the lion then the lion is kind.
((("someone" "needs" "lion" "+") ("someone" "sees" "lion" "+")) -> ("lion" "is" "kind" "+"))
If someone sees the dog then the dog is not round.
((("someone" "sees" "dog" "+")) -> ("dog" "is" "round" "-"))
If someone needs the cat and they do not see the dog then they visit the dog.
((("someone" "needs" "cat" "+") ("someone" "sees" "dog" "~")) -> ("someone" "visits" "dog" "+"))
If someone sees the cat then they visit the dog.
((("someone" "sees" "cat" "+")) -> ("someone" "visits" "dog" "+"))
If the lion visits the dog then the lion sees the cat.
((("lion" "visits" "dog" "+")) -> ("lion" "sees" "cat" "+"))
The dog is big.
True
1
proof
[(triple7)]
("dog" "is" "big" "+")
triple7
The cat does not see the lion.
False
1
inv-proof
[(triple5)]
("cat" "sees" "lion" "-")
triple5
The lion is kind.
True
3
proof
[(((triple4 triple5) -> rule4))]
("lion" "is" "kind" "+")
((triple4 triple5) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The dog does not need the dog.
False
2
inv-proof
[(((triple9) -> rule1))]
("dog" "needs" "dog" "-")
((triple9) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is not round.
True
3
proof
[(((((triple1) -> rule3)) -> rule5) OR ((((triple7) -> rule3)) -> rule5))]
("dog" "is" "round" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The dog is not round.
("dog" "is" "round" "-")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule5 % int1))
The dog is not round.
("dog" "is" "round" "-")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog is round.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5) OR ((((triple7) -> rule3)) -> rule5))]
("dog" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The dog is not round.
("dog" "is" "round" "-")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule5 % int1))
The dog is not round.
("dog" "is" "round" "-")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The lion does not see the cat.
Unknown
inv-rconc
[@2: The lion sees the cat.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("lion" "sees" "cat" "-")
The lion visits the dog.
Unknown
rconc
[@3: The lion visits the dog.[CWA. Example of deepest failure = (rule7 <- rule8 <- rule6 <- FAIL)]]
("lion" "visits" "dog" "+")
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "cold" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
@0: The cat does not need the dog.[(triple3)] The cat is big.[(triple1)] The cat is kind.[(triple2)] The cat needs the lion.[(triple4)] The cat sees the lion.[(triple5)] The cat visits the dog.[(triple6)] The dog is big.[(triple7)] The dog needs the lion.[(triple8)] The dog visits the cat.[(triple9)] The dog visits the lion.[(triple10)] The lion does not visit the cat.[(triple15)] The lion is not rough.[(triple11)] The lion is round.[(triple12)] The lion needs the cat.[(triple13)] The lion needs the dog.[(triple14)] @1: The cat sees the dog.[(((triple1) -> rule3))] The dog needs the dog.[(((triple9) -> rule1))] The dog sees the dog.[(((triple7) -> rule3))] The lion is kind.[(((triple4 triple5) -> rule4))] @2: The dog is not round.[(((((triple1) -> rule3)) -> rule5) OR ((((triple7) -> rule3)) -> rule5))]
The cat does not need the dog.
("cat" "needs" "dog" "-")
triple3
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat needs the lion.
("cat" "needs" "lion" "+")
triple4
The cat sees the lion.
("cat" "sees" "lion" "+")
triple5
The cat visits the dog.
("cat" "visits" "dog" "+")
triple6
The dog is big.
("dog" "is" "big" "+")
triple7
The dog needs the lion.
("dog" "needs" "lion" "+")
triple8
The dog visits the cat.
("dog" "visits" "cat" "+")
triple9
The dog visits the lion.
("dog" "visits" "lion" "+")
triple10
The lion does not visit the cat.
("lion" "visits" "cat" "-")
triple15
The lion is not rough.
("lion" "is" "rough" "-")
triple11
The lion is round.
("lion" "is" "round" "+")
triple12
The lion needs the cat.
("lion" "needs" "cat" "+")
triple13
The lion needs the dog.
("lion" "needs" "dog" "+")
triple14
The cat sees the dog.
("cat" "sees" "dog" "+")
((triple1) -> (rule3 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple9) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple7) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((triple4 triple5) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The dog is not round.
("dog" "is" "round" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The dog is not round.
("dog" "is" "round" "-")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule5 % int1))
The dog is not round.
("dog" "is" "round" "-")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2