The cat is red. The cat does not need the lion. The lion eats the cat. The lion is blue. The lion is round. The lion does not like the cat. The lion needs the cat. If something eats the cat then it is not rough. If the lion likes the cat then the lion needs the cat. If something needs the cat and it does not like the cat then it likes the lion. If something is blue then it likes the lion. If something likes the cat then the cat eats the lion. If the cat needs the lion and the cat is not round then the cat eats the lion. If something likes the lion then the lion is kind. If something is kind then it does not need the lion.
The cat is red.
("cat" "is" "red" "+")
The cat does not need the lion.
("cat" "needs" "lion" "-")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is round.
("lion" "is" "round" "+")
The lion does not like the cat.
("lion" "likes" "cat" "-")
The lion needs the cat.
("lion" "needs" "cat" "+")
If something eats the cat then it is not rough.
((("something" "eats" "cat" "+")) -> ("something" "is" "rough" "-"))
If the lion likes the cat then the lion needs the cat.
((("lion" "likes" "cat" "+")) -> ("lion" "needs" "cat" "+"))
If something needs the cat and it does not like the cat then it likes the lion.
((("something" "needs" "cat" "+") ("something" "likes" "cat" "~")) -> ("something" "likes" "lion" "+"))
If something is blue then it likes the lion.
((("something" "is" "blue" "+")) -> ("something" "likes" "lion" "+"))
If something likes the cat then the cat eats the lion.
((("something" "likes" "cat" "+")) -> ("cat" "eats" "lion" "+"))
If the cat needs the lion and the cat is not round then the cat eats the lion.
((("cat" "needs" "lion" "+") ("cat" "is" "round" "~")) -> ("cat" "eats" "lion" "+"))
If something likes the lion then the lion is kind.
((("something" "likes" "lion" "+")) -> ("lion" "is" "kind" "+"))
If something is kind then it does not need the lion.
((("something" "is" "kind" "+")) -> ("something" "needs" "lion" "-"))
The lion needs the cat.
True
1
proof
[(triple7)]
("lion" "needs" "cat" "+")
triple7
The lion does not eat the cat.
False
1
inv-proof
[(triple3)]
("lion" "eats" "cat" "-")
triple3
The lion likes the lion.
True
2
proof
[(((triple4) -> rule4) OR ((triple7 triple6) -> rule3))]
("lion" "likes" "lion" "+")
((triple4) -> (rule4 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
((triple7 triple6) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion does not like the lion.
False
2
inv-proof
[(((triple4) -> rule4) OR ((triple7 triple6) -> rule3))]
("lion" "likes" "lion" "-")
((triple4) -> (rule4 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
((triple7 triple6) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is kind.
True
3
proof
[(((((triple4) -> rule4)) -> rule7) OR ((((triple7 triple6) -> rule3)) -> rule7))]
("lion" "is" "kind" "+")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
((((triple7 triple6) -> (rule3 % int2))) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is not kind.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule7) OR ((((triple7 triple6) -> rule3)) -> rule7))]
("lion" "is" "kind" "-")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
((((triple7 triple6) -> (rule3 % int2))) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion does not need the lion.
True
4
proof
[(((((((triple4) -> rule4)) -> rule7)) -> rule8) OR ((((((triple7 triple6) -> rule3)) -> rule7)) -> rule8))]
("lion" "needs" "lion" "-")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The lion does not need the lion.
("lion" "needs" "lion" "-")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
((((((triple7 triple6) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The lion does not need the lion.
("lion" "needs" "lion" "-")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion needs the lion.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule7)) -> rule8) OR ((((((triple7 triple6) -> rule3)) -> rule7)) -> rule8))]
("lion" "needs" "lion" "+")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The lion does not need the lion.
("lion" "needs" "lion" "-")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
((((((triple7 triple6) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The lion does not need the lion.
("lion" "needs" "lion" "-")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The cat does not eat the lion.
Unknown
inv-rconc
[@1: The cat eats the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "eats" "lion" "-")
The cat likes the lion.
Unknown
rconc
[@1: The cat likes the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "likes" "lion" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The cat does not need the lion.[(triple2)] The cat is red.[(triple1)] The lion does not like the cat.[(triple6)] The lion eats the cat.[(triple3)] The lion is blue.[(triple4)] The lion is round.[(triple5)] The lion needs the cat.[(triple7)] @1: The lion is not rough.[(((triple3) -> rule1))] The lion likes the lion.[(((triple4) -> rule4) OR ((triple7 triple6) -> rule3))] @2: The lion is kind.[(((((triple4) -> rule4)) -> rule7) OR ((((triple7 triple6) -> rule3)) -> rule7))] @3: The lion does not need the lion.[(((((((triple4) -> rule4)) -> rule7)) -> rule8) OR ((((((triple7 triple6) -> rule3)) -> rule7)) -> rule8))]
The cat does not need the lion.
("cat" "needs" "lion" "-")
triple2
The cat is red.
("cat" "is" "red" "+")
triple1
The lion does not like the cat.
("lion" "likes" "cat" "-")
triple6
The lion eats the cat.
("lion" "eats" "cat" "+")
triple3
The lion is blue.
("lion" "is" "blue" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
triple5
The lion needs the cat.
("lion" "needs" "cat" "+")
triple7
The lion is not rough.
("lion" "is" "rough" "-")
((triple3) -> (rule1 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple4) -> (rule4 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
((triple7 triple6) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
((((triple7 triple6) -> (rule3 % int2))) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion does not need the lion.
("lion" "needs" "lion" "-")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The lion does not need the lion.
("lion" "needs" "lion" "-")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
((((((triple7 triple6) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The lion does not need the lion.
("lion" "needs" "lion" "-")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3