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