Charlie is white. Dave is white. Fiona is red. Harry is furry. If Dave is red then Dave is kind. If Dave is white then Dave is round. If someone is red then they are round. If someone is red then they are kind. If Harry is round then Harry is cold. All rough people are kind. Furry people are round. All red, round people are cold.
Charlie is white.
("Charlie" "is" "white" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If Dave is red then Dave is kind.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "kind" "+"))
If Dave is white then Dave is round.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "round" "+"))
If someone is red then they are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is red then they are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If Harry is round then Harry is cold.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "cold" "+"))
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
All red, round people are cold.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Charlie is white.
True
1
proof
[(triple1)]
("Charlie" "is" "white" "+")
triple1
Fiona is not red.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "red" "-")
triple3
Harry is round.
True
2
proof
[(((triple4) -> rule7))]
("Harry" "is" "round" "+")
((triple4) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple4) -> rule7))]
("Harry" "is" "round" "-")
((triple4) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Fiona is cold.
True
4
proof
[(((triple3 ((triple3) -> rule3)) -> rule8))]
("Fiona" "is" "cold" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Harry is not cold.
False
3
inv-proof
[(((((triple4) -> rule7)) -> rule5))]
("Harry" "is" "cold" "-")
((((triple4) -> (rule7 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "kind" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "cold" "+")
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "round" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Charlie is white.[(triple1)] Dave is white.[(triple2)] Fiona is red.[(triple3)] Harry is furry.[(triple4)] @1: Dave is round.[(((triple2) -> rule2))] Fiona is kind.[(((triple3) -> rule4))] Fiona is round.[(((triple3) -> rule3))] Harry is round.[(((triple4) -> rule7))] @2: Fiona is cold.[(((triple3 ((triple3) -> rule3)) -> rule8))] Harry is cold.[(((((triple4) -> rule7)) -> rule5))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
((triple2) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple3) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple3) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple4) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((triple4) -> (rule7 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2