Charlie is cold. Charlie is quiet. Dave is furry. Dave is green. Dave is not nice. Dave is quiet. Fiona is cold. Fiona is not furry. Fiona is nice. Harry is quiet. If something is nice then it is white. If Charlie is round and Charlie is not cold then Charlie is furry. If something is white then it is round. If something is nice and not white then it is not green. If something is round and not quiet then it is not green. If something is nice then it is green.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is not furry.
("Fiona" "is" "furry" "-")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is nice then it is white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If Charlie is round and Charlie is not cold then Charlie is furry.
((("Charlie" "is" "round" "+") ("Charlie" "is" "cold" "~")) -> ("Charlie" "is" "furry" "+"))
If something is white then it is round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
If something is nice and not white then it is not green.
((("something" "is" "nice" "+") ("something" "is" "white" "~")) -> ("something" "is" "green" "-"))
If something is round and not quiet then it is not green.
((("something" "is" "round" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "green" "-"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Fiona is nice.
True
1
proof
[(triple9)]
("Fiona" "is" "nice" "+")
triple9
Dave is not furry.
False
1
inv-proof
[(triple3)]
("Dave" "is" "furry" "-")
triple3
Fiona is white.
True
2
proof
[(((triple9) -> rule1))]
("Fiona" "is" "white" "+")
((triple9) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is not green.
False
2
inv-proof
[(((triple9) -> rule6))]
("Fiona" "is" "green" "-")
((triple9) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "white" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "white" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Charlie is cold.[(triple1)] Charlie is quiet.[(triple2)] Dave is furry.[(triple3)] Dave is green.[(triple4)] Dave is not nice.[(triple5)] Dave is quiet.[(triple6)] Fiona is cold.[(triple7)] Fiona is nice.[(triple9)] Fiona is not furry.[(triple8)] Harry is quiet.[(triple10)] @1: Fiona is green.[(((triple9) -> rule6))] Fiona is white.[(((triple9) -> rule1))] @2: Fiona is round.[(((((triple9) -> rule1)) -> rule3))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is not nice.
("Dave" "is" "nice" "-")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
Fiona is not furry.
("Fiona" "is" "furry" "-")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Fiona is green.
("Fiona" "is" "green" "+")
((triple9) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple9) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2