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