Anne is smart. Bob is green. Harry is smart. Big things are smart. If Harry is quiet and Harry is white then Harry is nice. Quiet, smart things are green. All quiet things are nice. All rough things are smart. Green things are rough.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is green.
("Bob" "is" "green" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If Harry is quiet and Harry is white then Harry is nice.
((("Harry" "is" "quiet" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "nice" "+"))
Quiet, smart things are green.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All quiet things are nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
All rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Anne is smart.
True
1
proof
[(triple1)]
("Anne" "is" "smart" "+")
triple1
Bob is not green.
False
1
inv-proof
[(triple2)]
("Bob" "is" "green" "-")
triple2
Bob is rough.
True
2
proof
[(((triple2) -> rule6))]
("Bob" "is" "rough" "+")
((triple2) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple2) -> rule6))]
("Bob" "is" "rough" "-")
((triple2) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "nice" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "green" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Anne is smart.[(triple1)] Bob is green.[(triple2)] Harry is smart.[(triple3)] @1: Bob is rough.[(((triple2) -> rule6))] @2: Bob is smart.[(((((triple2) -> rule6)) -> rule5))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
((triple2) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2