Dave is cold. Erin is blue. Gary is kind. If something is blue then it is not round. Cold, green things are round. Green things are round. Rough things are cold. If Dave is round then Dave is furry. If something is furry and blue then it is kind. Cold things are green. If something is cold and not blue then it is rough.
Dave is cold.
("Dave" "is" "cold" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If something is blue then it is not round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "-"))
Cold, green things are round.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If Dave is round then Dave is furry.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "furry" "+"))
If something is furry and blue then it is kind.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is cold and not blue then it is rough.
((("something" "is" "cold" "+") ("something" "is" "blue" "~")) -> ("something" "is" "rough" "+"))
Dave is cold.
True
1
proof
[(triple1)]
("Dave" "is" "cold" "+")
triple1
Dave is not cold.
False
1
inv-proof
[(triple1)]
("Dave" "is" "cold" "-")
triple1
Dave is green.
True
2
proof
[(((triple1) -> rule7))]
("Dave" "is" "green" "+")
((triple1) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple1) -> rule7))]
("Dave" "is" "green" "-")
((triple1) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
True
3
proof
[(((((triple1) -> rule7)) -> rule3) OR ((triple1 ((triple1) -> rule7)) -> rule2))]
("Dave" "is" "round" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((triple1 ((triple1) -> (rule7 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not round.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule3) OR ((triple1 ((triple1) -> rule7)) -> rule2))]
("Dave" "is" "round" "-")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((triple1 ((triple1) -> (rule7 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
True
4
proof
[(((((((triple1) -> rule7)) -> rule3)) -> rule5) OR ((((triple1 ((triple1) -> rule7)) -> rule2)) -> rule5))]
("Dave" "is" "furry" "+")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
((((triple1 ((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not furry.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule3)) -> rule5) OR ((((triple1 ((triple1) -> rule7)) -> rule2)) -> rule5))]
("Dave" "is" "furry" "-")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
((((triple1 ((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is green.
Unknown
rconc
[@3: Gary is green.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule8 <- FAIL)]]
("Gary" "is" "green" "+")
Erin is not cold.
Unknown
inv-rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Erin" "is" "cold" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "rough" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Dave is cold.[(triple1)] Erin is blue.[(triple2)] Gary is kind.[(triple3)] @1: Dave is green.[(((triple1) -> rule7))] Erin is not round.[(((triple2) -> rule1))] @2: Dave is round.[(((((triple1) -> rule7)) -> rule3) OR ((triple1 ((triple1) -> rule7)) -> rule2))] @3: Dave is furry.[(((((((triple1) -> rule7)) -> rule3)) -> rule5) OR ((((triple1 ((triple1) -> rule7)) -> rule2)) -> rule5))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
((triple1) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Erin is not round.
("Erin" "is" "round" "-")
((triple2) -> (rule1 % int1))
Erin is not round.
("Erin" "is" "round" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((triple1 ((triple1) -> (rule7 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
((((triple1 ((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3