Dave is round. Erin is cold. Gary is furry. If something is smart and blue then it is kind. All kind, cold things are young. All furry things are cold. Furry, cold things are smart. Kind things are blue. Kind things are furry. If something is smart and furry then it is young. Young, smart things are blue.
Dave is round.
("Dave" "is" "round" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
If something is smart and blue then it is kind.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
All kind, cold things are young.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
All furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Furry, cold things are smart.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If something is smart and furry then it is young.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Young, smart things are blue.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Erin is cold.
True
1
proof
[(triple2)]
("Erin" "is" "cold" "+")
triple2
Dave is not round.
False
1
inv-proof
[(triple1)]
("Dave" "is" "round" "-")
triple1
Gary is cold.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "cold" "-")
((triple3) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
True
4
proof
[(((triple3 ((triple3) -> rule3)) -> rule4))]
("Gary" "is" "smart" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not smart.
False
4
inv-proof
[(((triple3 ((triple3) -> rule3)) -> rule4))]
("Gary" "is" "smart" "-")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is young.
True
6
proof
[(((((triple3 ((triple3) -> rule3)) -> rule4) triple3) -> rule7))]
("Gary" "is" "young" "+")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule4 % int2)) triple3) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not young.
False
6
inv-proof
[(((((triple3 ((triple3) -> rule3)) -> rule4) triple3) -> rule7))]
("Gary" "is" "young" "-")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule4 % int2)) triple3) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Dave is not smart.
Unknown
inv-rconc
[@3: Dave is smart.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule1 <- FAIL)]]
("Dave" "is" "smart" "-")
Erin is young.
Unknown
rconc
[@4: Erin is young.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule4 <- rule6 <- FAIL)]]
("Erin" "is" "young" "+")
Dave is not furry.
Unknown
inv-rconc
[@3: Dave is furry.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule4 <- FAIL)]]
("Dave" "is" "furry" "-")
Erin is smart.
Unknown
rconc
[@3: Erin is smart.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule1 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Dave is round.[(triple1)] Erin is cold.[(triple2)] Gary is furry.[(triple3)] @1: Gary is cold.[(((triple3) -> rule3))] @2: Gary is smart.[(((triple3 ((triple3) -> rule3)) -> rule4))] @3: Gary is young.[(((((triple3 ((triple3) -> rule3)) -> rule4) triple3) -> rule7))] @4: Gary is blue.[(((((((triple3 ((triple3) -> rule3)) -> rule4) triple3) -> rule7) ((triple3 ((triple3) -> rule3)) -> rule4)) -> rule8))] @5: Gary is kind.[(((((triple3 ((triple3) -> rule3)) -> rule4) ((((((triple3 ((triple3) -> rule3)) -> rule4) triple3) -> rule7) ((triple3 ((triple3) -> rule3)) -> rule4)) -> rule8)) -> rule1))]
Dave is round.
("Dave" "is" "round" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule4 % int2)) triple3) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple3 ((triple3) -> (rule3 % int4))) -> (rule4 % int3)) triple3) -> (rule7 % int2)) ((triple3 ((triple3) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is kind.
("Gary" "is" "kind" "+")
((((triple3 ((triple3) -> (rule3 % int5))) -> (rule4 % int4)) ((((((triple3 ((triple3) -> (rule3 % int5))) -> (rule4 % int4)) triple3) -> (rule7 % int3)) ((triple3 ((triple3) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule8 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
int5