Charlie is big. Dave is quiet. Erin is quiet. Fiona is quiet. If something is kind and not red then it is young. Big things are young. If something is quiet then it is kind. Young things are kind. If something is red and not quiet then it is not blue. If Charlie is white then Charlie is young.
Charlie is big.
("Charlie" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If something is kind and not red then it is young.
((("something" "is" "kind" "+") ("something" "is" "red" "~")) -> ("something" "is" "young" "+"))
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is quiet then it is kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something is red and not quiet then it is not blue.
((("something" "is" "red" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "blue" "-"))
If Charlie is white then Charlie is young.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "young" "+"))
Erin is quiet.
True
1
proof
[(triple3)]
("Erin" "is" "quiet" "+")
triple3
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Fiona is kind.
True
2
proof
[(((triple4) -> rule3))]
("Fiona" "is" "kind" "+")
((triple4) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "kind" "-")
((triple2) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Charlie is kind.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("Charlie" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not kind.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("Charlie" "is" "kind" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "young" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "young" "+")
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Charlie is big.[(triple1)] Dave is quiet.[(triple2)] Erin is quiet.[(triple3)] Fiona is quiet.[(triple4)] @1: Charlie is young.[(((triple1) -> rule2))] Dave is kind.[(((triple2) -> rule3))] Erin is kind.[(((triple3) -> rule3))] Fiona is kind.[(((triple4) -> rule3))] @2: Charlie is kind.[(((((triple1) -> rule2)) -> rule4))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple4) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2