Anne is blue. Dave is not smart. Harry is big. Round people are smart. All young, blue people are not smart. Big, round people are not blue. Round people are white. Young people are not green. Big people are round.
Anne is blue.
("Anne" "is" "blue" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
Harry is big.
("Harry" "is" "big" "+")
Round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
All young, blue people are not smart.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "-"))
Big, round people are not blue.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "-"))
Round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Young people are not green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "-"))
Big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Harry is not big.
False
1
inv-proof
[(triple3)]
("Harry" "is" "big" "-")
triple3
Harry is round.
True
2
proof
[(((triple3) -> rule6))]
("Harry" "is" "round" "+")
((triple3) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple3) -> rule6))]
("Harry" "is" "round" "-")
((triple3) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
True
3
proof
[(((((triple3) -> rule6)) -> rule4))]
("Harry" "is" "white" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
False
4
inv-proof
[(((triple3 ((triple3) -> rule6)) -> rule3))]
("Harry" "is" "blue" "+")
((triple3 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Anne is not smart.
Unknown
inv-rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "round" "+")
Dave is not white.
Unknown
inv-rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Dave" "is" "white" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is blue.[(triple1)] Dave is not smart.[(triple2)] Harry is big.[(triple3)] @1: Harry is round.[(((triple3) -> rule6))] @2: Harry is not blue.[(((triple3 ((triple3) -> rule6)) -> rule3))] Harry is smart.[(((((triple3) -> rule6)) -> rule1))] Harry is white.[(((((triple3) -> rule6)) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Dave is not smart.
("Dave" "is" "smart" "-")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
((triple3) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
((triple3 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2