Anne is young. Fiona is quiet. Gary is quiet. Harry is not white. Young people are quiet. If someone is quiet then they are white. If someone is white and young then they are cold.
Anne is young.
("Anne" "is" "young" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is not white.
("Harry" "is" "white" "-")
Young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is white and young then they are cold.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Anne is young.
True
1
proof
[(triple1)]
("Anne" "is" "young" "+")
triple1
Harry is white.
False
1
inv-proof
[(triple4)]
("Harry" "is" "white" "+")
triple4
Gary is white.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "white" "+")
((triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "white" "-")
((triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Anne" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not white.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Anne" "is" "white" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
True
5
proof
[(((((((triple1) -> rule1)) -> rule2) triple1) -> rule3))]
("Anne" "is" "cold" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not cold.
False
5
inv-proof
[(((((((triple1) -> rule1)) -> rule2) triple1) -> rule3))]
("Anne" "is" "cold" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "cold" "-")
Harry is quiet.
Unknown
rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "quiet" "+")
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "cold" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "cold" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Anne is young.[(triple1)] Fiona is quiet.[(triple2)] Gary is quiet.[(triple3)] Harry is not white.[(triple4)] @1: Anne is quiet.[(((triple1) -> rule1))] Fiona is white.[(((triple2) -> rule2))] Gary is white.[(((triple3) -> rule2))] @2: Anne is white.[(((((triple1) -> rule1)) -> rule2))] @3: Anne is cold.[(((((((triple1) -> rule1)) -> rule2) triple1) -> rule3))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Harry is not white.
("Harry" "is" "white" "-")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple2) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3