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