Dave is cold. Erin is blue. Erin is cold. Erin is round. Gary is cold. Harry is blue. Harry is kind. Furry, cold people are young. If Erin is cold then Erin is kind. If someone is kind and rough then they are furry. If someone is young then they are furry. Round people are rough. If someone is young then they are furry.
Dave is cold.
("Dave" "is" "cold" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Furry, cold people are young.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If Erin is cold then Erin is kind.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "kind" "+"))
If someone is kind and rough then they are furry.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If someone is young then they are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If someone is young then they are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Dave is cold.
True
1
proof
[(triple1)]
("Dave" "is" "cold" "+")
triple1
Erin is not round.
False
1
inv-proof
[(triple4)]
("Erin" "is" "round" "-")
triple4
Erin is kind.
True
2
proof
[(((triple3) -> rule2))]
("Erin" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not rough.
False
2
inv-proof
[(((triple4) -> rule5))]
("Erin" "is" "rough" "-")
((triple4) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
True
5
proof
[(((((triple3) -> rule2) ((triple4) -> rule5)) -> rule3))]
("Erin" "is" "furry" "+")
((((triple3) -> (rule2 % int3)) ((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not furry.
False
5
inv-proof
[(((((triple3) -> rule2) ((triple4) -> rule5)) -> rule3))]
("Erin" "is" "furry" "-")
((((triple3) -> (rule2 % int3)) ((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is young.
True
7
proof
[(((((((triple3) -> rule2) ((triple4) -> rule5)) -> rule3) triple3) -> rule1))]
("Erin" "is" "young" "+")
((((((triple3) -> (rule2 % int4)) ((triple4) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is not young.
False
7
inv-proof
[(((((((triple3) -> rule2) ((triple4) -> rule5)) -> rule3) triple3) -> rule1))]
("Erin" "is" "young" "-")
((((((triple3) -> (rule2 % int4)) ((triple4) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "rough" "-")
Gary is furry.
Unknown
rconc
[@3: Gary is furry.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule3 <- FAIL)]]
("Gary" "is" "furry" "+")
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Dave" "is" "young" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "rough" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Dave is cold.[(triple1)] Erin is blue.[(triple2)] Erin is cold.[(triple3)] Erin is round.[(triple4)] Gary is cold.[(triple5)] Harry is blue.[(triple6)] Harry is kind.[(triple7)] @1: Erin is kind.[(((triple3) -> rule2))] Erin is rough.[(((triple4) -> rule5))] @2: Erin is furry.[(((((triple3) -> rule2) ((triple4) -> rule5)) -> rule3))] @3: Erin is young.[(((((((triple3) -> rule2) ((triple4) -> rule5)) -> rule3) triple3) -> rule1))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple4) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple3) -> (rule2 % int3)) ((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
((((((triple3) -> (rule2 % int4)) ((triple4) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4