Charlie is round. Erin is rough. Cold things are rough. Furry things are white. If Charlie is round and Charlie is white then Charlie is furry. If Charlie is red then Charlie is furry. Cold, furry things are not young. All furry, rough things are young. If something is young and not rough then it is not round. All round things are red.
Charlie is round.
("Charlie" "is" "round" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Furry things are white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If Charlie is round and Charlie is white then Charlie is furry.
((("Charlie" "is" "round" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "furry" "+"))
If Charlie is red then Charlie is furry.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "furry" "+"))
Cold, furry things are not young.
((("something" "is" "cold" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "-"))
All furry, rough things are young.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is young and not rough then it is not round.
((("something" "is" "young" "+") ("something" "is" "rough" "~")) -> ("something" "is" "round" "-"))
All round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Charlie is round.
True
1
proof
[(triple1)]
("Charlie" "is" "round" "+")
triple1
Erin is not rough.
False
1
inv-proof
[(triple2)]
("Erin" "is" "rough" "-")
triple2
Charlie is red.
True
2
proof
[(((triple1) -> rule8))]
("Charlie" "is" "red" "+")
((triple1) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple1) -> rule8))]
("Charlie" "is" "red" "-")
((triple1) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
True
3
proof
[(((((triple1) -> rule8)) -> rule4))]
("Charlie" "is" "furry" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not furry.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule4))]
("Charlie" "is" "furry" "-")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "rough" "-")
Erin is red.
Unknown
rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "red" "+")
Charlie is not young.
Unknown
inv-rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "young" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Charlie is round.[(triple1)] Erin is rough.[(triple2)] @1: Charlie is red.[(((triple1) -> rule8))] @2: Charlie is furry.[(((((triple1) -> rule8)) -> rule4))] @3: Charlie is white.[(((((((triple1) -> rule8)) -> rule4)) -> rule2))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3