Charlie is furry. Dave is not round. Erin is young. Gary is cold. Gary is green. Gary is rough. Gary is young. If Dave is round then Dave is cold. If someone is round and rough then they are green. If someone is blue and not cold then they are furry. If someone is blue then they are furry. Rough people are furry. If someone is cold and green then they are rough. Young people are rough. If Erin is furry then Erin is not green.
Charlie is furry.
("Charlie" "is" "furry" "+")
Dave is not round.
("Dave" "is" "round" "-")
Erin is young.
("Erin" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
If Dave is round then Dave is cold.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "cold" "+"))
If someone is round and rough then they are green.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone is blue and not cold then they are furry.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "furry" "+"))
If someone is blue then they are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Rough people are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If someone is cold and green then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Young people are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If Erin is furry then Erin is not green.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "green" "-"))
Gary is rough.
True
1
proof
[(triple6 OR ((triple7) -> rule7) OR ((triple4 triple5) -> rule6))]
("Gary" "is" "rough" "+")
triple6
((triple7) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple4 triple5) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Dave is round.
False
1
inv-proof
[(triple2)]
("Dave" "is" "round" "+")
triple2
Erin is rough.
True
2
proof
[(((triple3) -> rule7))]
("Erin" "is" "rough" "+")
((triple3) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple6) -> rule5) OR ((((triple7) -> rule7)) -> rule5) OR ((((triple4 triple5) -> rule6)) -> rule5))]
("Gary" "is" "furry" "-")
((triple6) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple7) -> (rule7 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple4 triple5) -> (rule6 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Erin is furry.
True
3
proof
[(((((triple3) -> rule7)) -> rule5))]
("Erin" "is" "furry" "+")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not furry.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule5))]
("Erin" "is" "furry" "-")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not green.
True
4
proof
[(((((((triple3) -> rule7)) -> rule5)) -> rule8))]
("Erin" "is" "green" "-")
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is green.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule5)) -> rule8))]
("Erin" "is" "green" "+")
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "+")
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "rough" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Charlie is furry.[(triple1)] Dave is not round.[(triple2)] Erin is young.[(triple3)] Gary is cold.[(triple4)] Gary is green.[(triple5)] Gary is rough.[(triple6 OR ((triple7) -> rule7) OR ((triple4 triple5) -> rule6))] Gary is young.[(triple7)] @1: Erin is rough.[(((triple3) -> rule7))] Gary is furry.[(((triple6) -> rule5) OR ((((triple7) -> rule7)) -> rule5) OR ((((triple4 triple5) -> rule6)) -> rule5))] @2: Erin is furry.[(((((triple3) -> rule7)) -> rule5))] @3: Erin is not green.[(((((((triple3) -> rule7)) -> rule5)) -> rule8))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Dave is not round.
("Dave" "is" "round" "-")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
((triple7) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple4 triple5) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
((triple3) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple6) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple7) -> (rule7 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple4 triple5) -> (rule6 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not green.
("Erin" "is" "green" "-")
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3