Anne is quiet. Anne is white. Bob is big. Bob is green. Bob is quiet. Charlie is blue. Erin is nice. All green things are nice. If something is green and not round then it is nice. If Bob is not green then Bob is quiet. If something is green and nice then it is blue. If something is green and blue then it is white. If something is quiet and not blue then it is not big.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is green and not round then it is nice.
((("something" "is" "green" "+") ("something" "is" "round" "~")) -> ("something" "is" "nice" "+"))
If Bob is not green then Bob is quiet.
((("Bob" "is" "green" "~")) -> ("Bob" "is" "quiet" "+"))
If something is green and nice then it is blue.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If something is green and blue then it is white.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If something is quiet and not blue then it is not big.
((("something" "is" "quiet" "+") ("something" "is" "blue" "~")) -> ("something" "is" "big" "-"))
Anne is white.
True
1
proof
[(triple2)]
("Anne" "is" "white" "+")
triple2
Bob is not green.
False
1
inv-proof
[(triple4)]
("Bob" "is" "green" "-")
triple4
Bob is nice.
True
2
proof
[(((triple4) -> rule1))]
("Bob" "is" "nice" "+")
((triple4) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple4) -> rule1))]
("Bob" "is" "nice" "-")
((triple4) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
True
4
proof
[(((triple4 ((triple4) -> rule1)) -> rule4))]
("Bob" "is" "blue" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not blue.
False
4
inv-proof
[(((triple4 ((triple4) -> rule1)) -> rule4))]
("Bob" "is" "blue" "-")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "white" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "nice" "+")
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "blue" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Anne is quiet.[(triple1)] Anne is white.[(triple2)] Bob is big.[(triple3)] Bob is green.[(triple4)] Bob is quiet.[(triple5)] Charlie is blue.[(triple6)] Erin is nice.[(triple7)] @1: Bob is nice.[(((triple4) -> rule1))] @2: Bob is blue.[(((triple4 ((triple4) -> rule1)) -> rule4))] @3: Bob is white.[(((triple4 ((triple4 ((triple4) -> rule1)) -> rule4)) -> rule5))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Bob is big.
("Bob" "is" "big" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple7
Bob is nice.
("Bob" "is" "nice" "+")
((triple4) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((triple4 ((triple4 ((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3