Charlie is smart. Dave is blue. Erin is white. Fiona is smart. All smart people are nice. Nice people are not quiet. If someone is rough and quiet then they are not blue. Rough, nice people are not young. If someone is smart and not quiet then they are young. If someone is quiet and not young then they are white.
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Nice people are not quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "-"))
If someone is rough and quiet then they are not blue.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "-"))
Rough, nice people are not young.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "-"))
If someone is smart and not quiet then they are young.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "young" "+"))
If someone is quiet and not young then they are white.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "white" "+"))
Erin is white.
True
1
proof
[(triple3)]
("Erin" "is" "white" "+")
triple3
Charlie is not smart.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "smart" "-")
triple1
Fiona is nice.
True
2
proof
[(((triple4) -> rule1))]
("Fiona" "is" "nice" "+")
((triple4) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not nice.
False
2
inv-proof
[(((triple4) -> rule1))]
("Fiona" "is" "nice" "-")
((triple4) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Charlie is not quiet.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Charlie" "is" "quiet" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "white" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "young" "+")
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "white" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Charlie is smart.[(triple1)] Dave is blue.[(triple2)] Erin is white.[(triple3)] Fiona is smart.[(triple4)] @1: Charlie is nice.[(((triple1) -> rule1))] Fiona is nice.[(((triple4) -> rule1))] @2: Charlie is not quiet.[(((((triple1) -> rule1)) -> rule2))] Fiona is not quiet.[(((((triple4) -> rule1)) -> rule2))] @3: Charlie is young.[(((triple1 ((((triple1) -> rule1)) -> rule2)) -> rule5))] Fiona is young.[(((triple4 ((((triple4) -> rule1)) -> rule2)) -> rule5))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple4) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
((triple4 ((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3