Anne is nice. Anne is red. Anne is white. Bob is not quiet. Charlie is not big. Charlie is cold. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is white. Dave is nice. Dave is not red. If something is white then it is cold. If Anne is nice then Anne is not big. Kind, cold things are nice. Red, cold things are nice. If something is kind and not cold then it is nice. All kind things are not nice.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not red.
("Dave" "is" "red" "-")
If something is white then it is cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If Anne is nice then Anne is not big.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "big" "-"))
Kind, cold things are nice.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Red, cold things are nice.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is kind and not cold then it is nice.
((("something" "is" "kind" "+") ("something" "is" "cold" "~")) -> ("something" "is" "nice" "+"))
All kind things are not nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "-"))
Dave is nice.
True
1
proof
[(triple11)]
("Dave" "is" "nice" "+")
triple11
Dave is red.
False
1
inv-proof
[(triple12)]
("Dave" "is" "red" "+")
triple12
Anne is cold.
True
2
proof
[(((triple3) -> rule1))]
("Anne" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
False
2
inv-proof
[(((triple1) -> rule2) OR ((((triple2 ((triple3) -> rule1)) -> rule4)) -> rule2))]
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
((((triple2 ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is cold.
Unknown
rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "cold" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is nice.[(triple1 OR ((triple2 ((triple3) -> rule1)) -> rule4))] Anne is red.[(triple2)] Anne is white.[(triple3)] Bob is not quiet.[(triple4)] Charlie is cold.[(triple6 OR ((triple10) -> rule1))] Charlie is nice.[(triple7 OR ((triple9 triple6) -> rule4) OR ((triple9 ((triple10) -> rule1)) -> rule4))] Charlie is not big.[(triple5)] Charlie is quiet.[(triple8)] Charlie is red.[(triple9)] Charlie is white.[(triple10)] Dave is nice.[(triple11)] Dave is not red.[(triple12)] @1: Anne is cold.[(((triple3) -> rule1))] Anne is not big.[(((triple1) -> rule2) OR ((((triple2 ((triple3) -> rule1)) -> rule4)) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
((triple2 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
((triple10) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
((triple9 triple6) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple9 ((triple10) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not big.
("Charlie" "is" "big" "-")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
Charlie is red.
("Charlie" "is" "red" "+")
triple9
Charlie is white.
("Charlie" "is" "white" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
triple11
Dave is not red.
("Dave" "is" "red" "-")
triple12
Anne is cold.
("Anne" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not big.
("Anne" "is" "big" "-")
((triple1) -> (rule2 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
((((triple2 ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3