The bear does not see the cat. The cat is blue. The cat is not nice. The cat is round. The cat needs the bear. The cat does not see the bear. The cat does not visit the bear. If something needs the bear and it is round then it sees the cat. If something sees the bear and it needs the cat then it does not see the cat. If something sees the cat then it visits the cat. If something is blue and it needs the cat then the cat is not blue. If something sees the bear and the bear needs the cat then it is blue. If something sees the cat then it is cold.
The bear does not see the cat.
("bear" "sees" "cat" "-")
The cat is blue.
("cat" "is" "blue" "+")
The cat is not nice.
("cat" "is" "nice" "-")
The cat is round.
("cat" "is" "round" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cat does not see the bear.
("cat" "sees" "bear" "-")
The cat does not visit the bear.
("cat" "visits" "bear" "-")
If something needs the bear and it is round then it sees the cat.
((("something" "needs" "bear" "+") ("something" "is" "round" "+")) -> ("something" "sees" "cat" "+"))
If something sees the bear and it needs the cat then it does not see the cat.
((("something" "sees" "bear" "+") ("something" "needs" "cat" "+")) -> ("something" "sees" "cat" "-"))
If something sees the cat then it visits the cat.
((("something" "sees" "cat" "+")) -> ("something" "visits" "cat" "+"))
If something is blue and it needs the cat then the cat is not blue.
((("something" "is" "blue" "+") ("something" "needs" "cat" "+")) -> ("cat" "is" "blue" "-"))
If something sees the bear and the bear needs the cat then it is blue.
((("something" "sees" "bear" "+") ("bear" "needs" "cat" "+")) -> ("something" "is" "blue" "+"))
If something sees the cat then it is cold.
((("something" "sees" "cat" "+")) -> ("something" "is" "cold" "+"))
The cat is blue.
True
1
proof
[(triple2)]
("cat" "is" "blue" "+")
triple2
The cat is nice.
False
1
inv-proof
[(triple3)]
("cat" "is" "nice" "+")
triple3
The cat sees the cat.
True
3
proof
[(((triple5 triple4) -> rule1))]
("cat" "sees" "cat" "+")
((triple5 triple4) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat does not see the cat.
False
3
inv-proof
[(((triple5 triple4) -> rule1))]
("cat" "sees" "cat" "-")
((triple5 triple4) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is cold.
True
4
proof
[(((((triple5 triple4) -> rule1)) -> rule6))]
("cat" "is" "cold" "+")
((((triple5 triple4) -> (rule1 % int2))) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat does not visit the cat.
False
4
inv-proof
[(((((triple5 triple4) -> rule1)) -> rule3))]
("cat" "visits" "cat" "-")
((((triple5 triple4) -> (rule1 % int2))) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The bear does not visit the cat.
Unknown
inv-rconc
[@1: The bear visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "visits" "cat" "-")
The bear is blue.
Unknown
rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "blue" "+")
The bear is not cold.
Unknown
inv-rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "cold" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The bear needs the cat.
Unknown
random
[@0: The bear needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "cat" "+")
@0: The bear does not see the cat.[(triple1)] The cat does not see the bear.[(triple6)] The cat does not visit the bear.[(triple7)] The cat is blue.[(triple2)] The cat is not nice.[(triple3)] The cat is round.[(triple4)] The cat needs the bear.[(triple5)] @1: The cat sees the cat.[(((triple5 triple4) -> rule1))] @2: The cat is cold.[(((((triple5 triple4) -> rule1)) -> rule6))] The cat visits the cat.[(((((triple5 triple4) -> rule1)) -> rule3))]
The bear does not see the cat.
("bear" "sees" "cat" "-")
triple1
The cat does not see the bear.
("cat" "sees" "bear" "-")
triple6
The cat does not visit the bear.
("cat" "visits" "bear" "-")
triple7
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is not nice.
("cat" "is" "nice" "-")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat needs the bear.
("cat" "needs" "bear" "+")
triple5
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple5 triple4) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
((((triple5 triple4) -> (rule1 % int2))) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat visits the cat.
("cat" "visits" "cat" "+")
((((triple5 triple4) -> (rule1 % int2))) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2