Bob is green. Charlie is furry. Charlie is white. Erin is not red. Erin is smart. Fiona is green. Fiona is not nice. All smart, nice people are round. If someone is white then they are round. If someone is round and not white then they are green. If Fiona is round and Fiona is nice then Fiona is not smart. If someone is nice and not round then they are red. If someone is furry and round then they are not red.
Bob is green.
("Bob" "is" "green" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is not red.
("Erin" "is" "red" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is not nice.
("Fiona" "is" "nice" "-")
All smart, nice people are round.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is white then they are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If someone is round and not white then they are green.
((("someone" "is" "round" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "green" "+"))
If Fiona is round and Fiona is nice then Fiona is not smart.
((("Fiona" "is" "round" "+") ("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "smart" "-"))
If someone is nice and not round then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "red" "+"))
If someone is furry and round then they are not red.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "-"))
Charlie is white.
True
1
proof
[(triple3)]
("Charlie" "is" "white" "+")
triple3
Fiona is not green.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "green" "-")
triple6
Charlie is round.
True
2
proof
[(((triple3) -> rule2))]
("Charlie" "is" "round" "+")
((triple3) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple3) -> rule2))]
("Charlie" "is" "round" "-")
((triple3) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not red.
True
4
proof
[(((triple2 ((triple3) -> rule2)) -> rule6))]
("Charlie" "is" "red" "-")
((triple2 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is red.
False
4
inv-proof
[(((triple2 ((triple3) -> rule2)) -> rule6))]
("Charlie" "is" "red" "+")
((triple2 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "round" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "red" "+")
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "green" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is green.[(triple1)] Charlie is furry.[(triple2)] Charlie is white.[(triple3)] Erin is not red.[(triple4)] Erin is smart.[(triple5)] Fiona is green.[(triple6)] Fiona is not nice.[(triple7)] @1: Charlie is round.[(((triple3) -> rule2))] @2: Charlie is not red.[(((triple2 ((triple3) -> rule2)) -> rule6))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Erin is not red.
("Erin" "is" "red" "-")
triple4
Erin is smart.
("Erin" "is" "smart" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Fiona is not nice.
("Fiona" "is" "nice" "-")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
((triple3) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not red.
("Charlie" "is" "red" "-")
((triple2 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2