Anne is cold. Dave is rough. Harry is green. All cold, round people are green. If Harry is round and Harry is not rough then Harry is big. If Anne is young and Anne is rough then Anne is big. All green people are young. Young, big people are kind. If someone is cold then they are round.
Anne is cold.
("Anne" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is green.
("Harry" "is" "green" "+")
All cold, round people are green.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If Harry is round and Harry is not rough then Harry is big.
((("Harry" "is" "round" "+") ("Harry" "is" "rough" "~")) -> ("Harry" "is" "big" "+"))
If Anne is young and Anne is rough then Anne is big.
((("Anne" "is" "young" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "big" "+"))
All green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Young, big people are kind.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Dave is rough.
True
1
proof
[(triple2)]
("Dave" "is" "rough" "+")
triple2
Dave is not rough.
False
1
inv-proof
[(triple2)]
("Dave" "is" "rough" "-")
triple2
Anne is round.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "round" "+")
((triple1) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "round" "-")
((triple1) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Anne is kind.
Unknown
rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Anne" "is" "kind" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Anne is cold.[(triple1)] Dave is rough.[(triple2)] Harry is green.[(triple3)] @1: Anne is round.[(((triple1) -> rule6))] Harry is young.[(((triple3) -> rule4))] @2: Anne is green.[(((triple1 ((triple1) -> rule6)) -> rule1))] @3: Anne is young.[(((((triple1 ((triple1) -> rule6)) -> rule1)) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple3) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3