Charlie is blue. Charlie is young. Dave is blue. Dave is cold. Erin is blue. Erin is round. Gary is young. All cold, young things are round. All rough, blue things are round. All young, round things are rough. Rough things are kind. If something is blue then it is cold. All young, rough things are round.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
All cold, young things are round.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
All rough, blue things are round.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
All young, round things are rough.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is blue then it is cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
All young, rough things are round.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
Erin is round.
True
1
proof
[(triple6)]
("Erin" "is" "round" "+")
triple6
Dave is not blue.
False
1
inv-proof
[(triple3)]
("Dave" "is" "blue" "-")
triple3
Erin is cold.
True
2
proof
[(((triple5) -> rule5))]
("Erin" "is" "cold" "+")
((triple5) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple1) -> rule5))]
("Charlie" "is" "cold" "-")
((triple1) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is round.
True
4
proof
[(((((triple1) -> rule5) triple2) -> rule1))]
("Charlie" "is" "round" "+")
((((triple1) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not round.
False
4
inv-proof
[(((((triple1) -> rule5) triple2) -> rule1))]
("Charlie" "is" "round" "-")
((((triple1) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
True
6
proof
[(((triple2 ((((triple1) -> rule5) triple2) -> rule1)) -> rule3))]
("Charlie" "is" "rough" "+")
((triple2 ((((triple1) -> (rule5 % int3)) triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is not rough.
False
6
inv-proof
[(((triple2 ((((triple1) -> rule5) triple2) -> rule1)) -> rule3))]
("Charlie" "is" "rough" "-")
((triple2 ((((triple1) -> (rule5 % int3)) triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Gary is not round.
Unknown
inv-rconc
[@4: Gary is round.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule1 <- rule5 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is rough.
Unknown
rconc
[@3: Gary is rough.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule5 <- FAIL)]]
("Gary" "is" "rough" "+")
Dave is not kind.
Unknown
inv-rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Dave" "is" "kind" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "rough" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is blue.[(triple1)] Charlie is young.[(triple2)] Dave is blue.[(triple3)] Dave is cold.[(triple4 OR ((triple3) -> rule5))] Erin is blue.[(triple5)] Erin is round.[(triple6)] Gary is young.[(triple7)] @1: Charlie is cold.[(((triple1) -> rule5))] Erin is cold.[(((triple5) -> rule5))] @2: Charlie is round.[(((((triple1) -> rule5) triple2) -> rule1))] @3: Charlie is rough.[(((triple2 ((((triple1) -> rule5) triple2) -> rule1)) -> rule3))] @4: Charlie is kind.[(((((triple2 ((((triple1) -> rule5) triple2) -> rule1)) -> rule3)) -> rule4))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
((triple3) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple5) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((((triple1) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2 ((((triple1) -> (rule5 % int3)) triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2 ((((triple1) -> (rule5 % int4)) triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4