Bob is round. Charlie is cold. Dave is rough. Fiona is kind. If someone is green then they are round. Kind people are green. If someone is green and not white then they are red.
Bob is round.
("Bob" "is" "round" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is green and not white then they are red.
((("someone" "is" "green" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "red" "+"))
Fiona is kind.
True
1
proof
[(triple4)]
("Fiona" "is" "kind" "+")
triple4
Fiona is not kind.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "kind" "-")
triple4
Fiona is green.
True
2
proof
[(((triple4) -> rule2))]
("Fiona" "is" "green" "+")
((triple4) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is not green.
False
2
inv-proof
[(((triple4) -> rule2))]
("Fiona" "is" "green" "-")
((triple4) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is round.
True
3
proof
[(((((triple4) -> rule2)) -> rule1))]
("Fiona" "is" "round" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is not round.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule1))]
("Fiona" "is" "round" "-")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "green" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "round" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Bob is round.[(triple1)] Charlie is cold.[(triple2)] Dave is rough.[(triple3)] Fiona is kind.[(triple4)] @1: Fiona is green.[(((triple4) -> rule2))] @2: Fiona is round.[(((((triple4) -> rule2)) -> rule1))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Fiona is kind.
("Fiona" "is" "kind" "+")
triple4
Fiona is green.
("Fiona" "is" "green" "+")
((triple4) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2