Anne is nice. Anne is quiet. Bob is nice. Charlie is cold. Fiona is blue. Fiona is round. Fiona is young. If something is nice and white then it is quiet. If something is young and cold then it is blue. If Charlie is cold then Charlie is young.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If something is nice and white then it is quiet.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is young and cold then it is blue.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If Charlie is cold then Charlie is young.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "young" "+"))
Charlie is cold.
True
1
proof
[(triple4)]
("Charlie" "is" "cold" "+")
triple4
Fiona is not blue.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "blue" "-")
triple5
Charlie is young.
True
2
proof
[(((triple4) -> rule3))]
("Charlie" "is" "young" "+")
((triple4) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple4) -> rule3))]
("Charlie" "is" "young" "-")
((triple4) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
True
4
proof
[(((((triple4) -> rule3) triple4) -> rule2))]
("Charlie" "is" "blue" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not blue.
False
4
inv-proof
[(((((triple4) -> rule3) triple4) -> rule2))]
("Charlie" "is" "blue" "-")
((((triple4) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Anne is blue.
Unknown
rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "blue" "+")
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is nice.[(triple1)] Anne is quiet.[(triple2)] Bob is nice.[(triple3)] Charlie is cold.[(triple4)] Fiona is blue.[(triple5)] Fiona is round.[(triple6)] Fiona is young.[(triple7)] @1: Charlie is young.[(((triple4) -> rule3))] @2: Charlie is blue.[(((((triple4) -> rule3) triple4) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
Fiona is round.
("Fiona" "is" "round" "+")
triple6
Fiona is young.
("Fiona" "is" "young" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
((triple4) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2