Anne is nice. Charlie is young. Gary is smart. Harry is quiet. If something is nice then it is rough. White things are not cold. All white things are not cold. Rough things are smart. Smart things are white. If something is cold and not white then it is young.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
White things are not cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "-"))
All white things are not cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "-"))
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is cold and not white then it is young.
((("something" "is" "cold" "+") ("something" "is" "white" "~")) -> ("something" "is" "young" "+"))
Harry is quiet.
True
1
proof
[(triple4)]
("Harry" "is" "quiet" "+")
triple4
Harry is not quiet.
False
1
inv-proof
[(triple4)]
("Harry" "is" "quiet" "-")
triple4
Gary is white.
True
2
proof
[(((triple3) -> rule5))]
("Gary" "is" "white" "+")
((triple3) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Anne is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "rough" "-")
((triple1) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not smart.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
True
4
proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule5))]
("Anne" "is" "white" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not white.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule5))]
("Anne" "is" "white" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Harry is not white.
Unknown
inv-rconc
[@3: Harry is white.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule1 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "young" "+")
Charlie is not smart.
Unknown
inv-rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "rough" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Anne is nice.[(triple1)] Charlie is young.[(triple2)] Gary is smart.[(triple3)] Harry is quiet.[(triple4)] @1: Anne is rough.[(((triple1) -> rule1))] Gary is white.[(((triple3) -> rule5))] @2: Anne is smart.[(((((triple1) -> rule1)) -> rule4))] Gary is not cold.[(((((triple3) -> rule5)) -> rule2) OR ((((triple3) -> rule5)) -> rule3))] @3: Anne is white.[(((((((triple1) -> rule1)) -> rule4)) -> rule5))] @4: Anne is not cold.[(((((((((triple1) -> rule1)) -> rule4)) -> rule5)) -> rule2) OR ((((((((triple1) -> rule1)) -> rule4)) -> rule5)) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Gary is not cold.
("Gary" "is" "cold" "-")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not cold.
("Anne" "is" "cold" "-")
((((((((triple1) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
((((((((triple1) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4