Charlie is young. Dave is not blue. Erin is smart. Gary is round. Blue things are quiet. Cold things are round. All round things are furry. All round, blue things are furry. All cold things are young. Smart things are cold.
Charlie is young.
("Charlie" "is" "young" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is round.
("Gary" "is" "round" "+")
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
All round things are furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
All round, blue things are furry.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
All cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Smart things are cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Dave is not blue.
True
1
proof
[(triple2)]
("Dave" "is" "blue" "-")
triple2
Gary is not round.
False
1
inv-proof
[(triple4)]
("Gary" "is" "round" "-")
triple4
Gary is furry.
True
2
proof
[(((triple4) -> rule3))]
("Gary" "is" "furry" "+")
((triple4) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple4) -> rule3))]
("Gary" "is" "furry" "-")
((triple4) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Erin is young.
True
3
proof
[(((((triple3) -> rule6)) -> rule5))]
("Erin" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not young.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule5))]
("Erin" "is" "young" "-")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
True
4
proof
[(((((((triple3) -> rule6)) -> rule2)) -> rule3))]
("Erin" "is" "furry" "+")
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not furry.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule2)) -> rule3))]
("Erin" "is" "furry" "-")
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Charlie" "is" "round" "-")
Dave is furry.
Unknown
rconc
[@3: Dave is furry.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule6 <- FAIL)]]
("Dave" "is" "furry" "+")
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "cold" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "quiet" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Charlie is young.[(triple1)] Dave is not blue.[(triple2)] Erin is smart.[(triple3)] Gary is round.[(triple4)] @1: Erin is cold.[(((triple3) -> rule6))] Gary is furry.[(((triple4) -> rule3))] @2: Erin is round.[(((((triple3) -> rule6)) -> rule2))] Erin is young.[(((((triple3) -> rule6)) -> rule5))] @3: Erin is furry.[(((((((triple3) -> rule6)) -> rule2)) -> rule3))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Dave is not blue.
("Dave" "is" "blue" "-")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple4) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3