Anne is big. Anne is not green. Anne is young. Bob is big. Charlie is nice. Charlie is round. Harry is big. If someone is blue then they are smart. All young people are blue. If someone is big and not round then they are not young.
Anne is big.
("Anne" "is" "big" "+")
Anne is not green.
("Anne" "is" "green" "-")
Anne is young.
("Anne" "is" "young" "+")
Bob is big.
("Bob" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
If someone is blue then they are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
All young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If someone is big and not round then they are not young.
((("someone" "is" "big" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "young" "-"))
Anne is young.
True
1
proof
[(triple3)]
("Anne" "is" "young" "+")
triple3
Anne is green.
False
1
inv-proof
[(triple2)]
("Anne" "is" "green" "+")
triple2
Anne is blue.
True
2
proof
[(((triple3) -> rule2))]
("Anne" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple3) -> rule2))]
("Anne" "is" "blue" "-")
((triple3) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("Anne" "is" "smart" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not smart.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("Anne" "is" "smart" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is smart.
Unknown
rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "smart" "+")
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "blue" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Anne is big.[(triple1)] Anne is not green.[(triple2)] Anne is young.[(triple3)] Bob is big.[(triple4)] Charlie is nice.[(triple5)] Charlie is round.[(triple6)] Harry is big.[(triple7)] @1: Anne is blue.[(((triple3) -> rule2))] @2: Anne is smart.[(((((triple3) -> rule2)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is not green.
("Anne" "is" "green" "-")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Anne is blue.
("Anne" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2