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