Anne is red. Dave is red. Fiona is smart. Harry is kind. If something is rough and red then it is big. If something is green then it is smart. If something is rough and red then it is kind. Green, rough things are big. Kind things are rough. All green, red things are smart. If Harry is rough and Harry is green then Harry is kind. All rough things are big.
Anne is red.
("Anne" "is" "red" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If something is rough and red then it is big.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is green then it is smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is rough and red then it is kind.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Green, rough things are big.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
All green, red things are smart.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If Harry is rough and Harry is green then Harry is kind.
((("Harry" "is" "rough" "+") ("Harry" "is" "green" "+")) -> ("Harry" "is" "kind" "+"))
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Harry is kind.
True
1
proof
[(triple4)]
("Harry" "is" "kind" "+")
triple4
Dave is not red.
False
1
inv-proof
[(triple2)]
("Dave" "is" "red" "-")
triple2
Harry is rough.
True
2
proof
[(((triple4) -> rule5))]
("Harry" "is" "rough" "+")
((triple4) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple4) -> rule5))]
("Harry" "is" "rough" "-")
((triple4) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
True
3
proof
[(((((triple4) -> rule5)) -> rule8))]
("Harry" "is" "big" "+")
((((triple4) -> (rule5 % int2))) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not big.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule8))]
("Harry" "is" "big" "-")
((((triple4) -> (rule5 % int2))) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Anne is not kind.
Unknown
inv-rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Anne" "is" "kind" "-")
Fiona is big.
Unknown
rconc
[@3: Fiona is big.[CWA. Example of deepest failure = (rule8 <- rule5 <- rule3 <- FAIL)]]
("Fiona" "is" "big" "+")
Anne is not rough.
Unknown
inv-rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Anne" "is" "rough" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Anne is red.[(triple1)] Dave is red.[(triple2)] Fiona is smart.[(triple3)] Harry is kind.[(triple4)] @1: Harry is rough.[(((triple4) -> rule5))] @2: Harry is big.[(((((triple4) -> rule5)) -> rule8))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is rough.
("Harry" "is" "rough" "+")
((triple4) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((((triple4) -> (rule5 % int2))) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2