Anne is nice. Anne is rough. Charlie is cold. Charlie is nice. Charlie is smart. Dave is green. Dave is rough. Smart things are green. Nice, rough things are green. All big, cold things are round.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Nice, rough things are green.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
All big, cold things are round.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Charlie is smart.
True
1
proof
[(triple5)]
("Charlie" "is" "smart" "+")
triple5
Charlie is not smart.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "smart" "-")
triple5
Charlie is green.
True
2
proof
[(((triple5) -> rule1))]
("Charlie" "is" "green" "+")
((triple5) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple5) -> rule1))]
("Charlie" "is" "green" "-")
((triple5) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "round" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Anne is nice.[(triple1)] Anne is rough.[(triple2)] Charlie is cold.[(triple3)] Charlie is nice.[(triple4)] Charlie is smart.[(triple5)] Dave is green.[(triple6)] Dave is rough.[(triple7)] @1: Anne is green.[(((triple1 triple2) -> rule2))] Charlie is green.[(((triple5) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple5) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1