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