Anne is blue. Anne is green. Anne is not white. Charlie is blue. Charlie is kind. Charlie is rough. Dave is not big. Dave is nice. Dave is rough. Harry is blue. Harry is not kind. Harry is white. If something is big and not white then it is nice. Green things are big. All big things are not kind.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is not white.
("Anne" "is" "white" "-")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is white.
("Harry" "is" "white" "+")
If something is big and not white then it is nice.
((("something" "is" "big" "+") ("something" "is" "white" "~")) -> ("something" "is" "nice" "+"))
Green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
All big things are not kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "-"))
Harry is not kind.
True
1
proof
[(triple11)]
("Harry" "is" "kind" "-")
triple11
Dave is not rough.
False
1
inv-proof
[(triple9)]
("Dave" "is" "rough" "-")
triple9
Anne is big.
True
2
proof
[(((triple2) -> rule2))]
("Anne" "is" "big" "+")
((triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple2) -> rule2))]
("Anne" "is" "big" "-")
((triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not kind.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Anne" "is" "kind" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is kind.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Anne" "is" "kind" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "big" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "big" "+")
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Anne is blue.[(triple1)] Anne is green.[(triple2)] Anne is not white.[(triple3)] Charlie is blue.[(triple4)] Charlie is kind.[(triple5)] Charlie is rough.[(triple6)] Dave is nice.[(triple8)] Dave is not big.[(triple7)] Dave is rough.[(triple9)] Harry is blue.[(triple10)] Harry is not kind.[(triple11)] Harry is white.[(triple12)] @1: Anne is big.[(((triple2) -> rule2))] @2: Anne is nice.[(((((triple2) -> rule2) triple3) -> rule1))] Anne is not kind.[(((((triple2) -> rule2)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is not white.
("Anne" "is" "white" "-")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Dave is nice.
("Dave" "is" "nice" "+")
triple8
Dave is not big.
("Dave" "is" "big" "-")
triple7
Dave is rough.
("Dave" "is" "rough" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Harry is not kind.
("Harry" "is" "kind" "-")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Anne is big.
("Anne" "is" "big" "+")
((triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple2) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not kind.
("Anne" "is" "kind" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2