Anne is not blue. Harry is not round. Harry is smart. If someone is big and not kind then they are white. If someone is round then they are not white. All smart, cold people are white. Smart people are cold. If Anne is big then Anne is round. If Harry is kind and Harry is big then Harry is blue.
Anne is not blue.
("Anne" "is" "blue" "-")
Harry is not round.
("Harry" "is" "round" "-")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is big and not kind then they are white.
((("someone" "is" "big" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "white" "+"))
If someone is round then they are not white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "-"))
All smart, cold people are white.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If Anne is big then Anne is round.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "round" "+"))
If Harry is kind and Harry is big then Harry is blue.
((("Harry" "is" "kind" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "blue" "+"))
Harry is not round.
True
1
proof
[(triple2)]
("Harry" "is" "round" "-")
triple2
Harry is round.
False
1
inv-proof
[(triple2)]
("Harry" "is" "round" "+")
triple2
Harry is cold.
True
2
proof
[(((triple3) -> rule4))]
("Harry" "is" "cold" "+")
((triple3) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple3) -> rule4))]
("Harry" "is" "cold" "-")
((triple3) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
True
4
proof
[(((triple3 ((triple3) -> rule4)) -> rule3))]
("Harry" "is" "white" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not white.
False
4
inv-proof
[(((triple3 ((triple3) -> rule4)) -> rule3))]
("Harry" "is" "white" "-")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "blue" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Anne is not blue.[(triple1)] Harry is not round.[(triple2)] Harry is smart.[(triple3)] @1: Harry is cold.[(((triple3) -> rule4))] @2: Harry is white.[(((triple3 ((triple3) -> rule4)) -> rule3))]
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Harry is not round.
("Harry" "is" "round" "-")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
((triple3) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2