Anne is red. Charlie is cold. Dave is cold. Green, young things are smart. If Charlie is quiet and Charlie is cold then Charlie is smart. Red things are smart. All quiet things are cold. Smart, rough things are green. All red things are cold. All cold things are rough. All young, rough things are smart.
Anne is red.
("Anne" "is" "red" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Green, young things are smart.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If Charlie is quiet and Charlie is cold then Charlie is smart.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "smart" "+"))
Red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
All quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Smart, rough things are green.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
All red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
All cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
All young, rough things are smart.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Dave is not cold.
False
1
inv-proof
[(triple3)]
("Dave" "is" "cold" "-")
triple3
Dave is rough.
True
2
proof
[(((triple3) -> rule7))]
("Dave" "is" "rough" "+")
((triple3) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple3) -> rule7))]
("Dave" "is" "rough" "-")
((triple3) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Charlie is not green.
Unknown
inv-rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "green" "-")
Dave is green.
Unknown
rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is red.[(triple1)] Charlie is cold.[(triple2)] Dave is cold.[(triple3)] @1: Anne is cold.[(((triple1) -> rule6))] Anne is smart.[(((triple1) -> rule3))] Charlie is rough.[(((triple2) -> rule7))] Dave is rough.[(((triple3) -> rule7))] @2: Anne is rough.[(((((triple1) -> rule6)) -> rule7))] @3: Anne is green.[(((((triple1) -> rule3) ((((triple1) -> rule6)) -> rule7)) -> rule5))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple3) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule6 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4