Anne is blue. Charlie is blue. Dave is green. Fiona is nice. All quiet, blue people are green. Smart people are young. All green people are nice. Young people are nice. Blue people are smart. If Charlie is smart and Charlie is blue then Charlie is quiet.
Anne is blue.
("Anne" "is" "blue" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
All quiet, blue people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
All green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is smart and Charlie is blue then Charlie is quiet.
((("Charlie" "is" "smart" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "quiet" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Dave is not green.
False
1
inv-proof
[(triple3)]
("Dave" "is" "green" "-")
triple3
Charlie is smart.
True
2
proof
[(((triple2) -> rule5))]
("Charlie" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple3) -> rule3))]
("Dave" "is" "nice" "-")
((triple3) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Anne is young.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("Anne" "is" "young" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2))]
("Charlie" "is" "young" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is nice.
True
4
proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule4) OR ((((((((triple2) -> rule5) triple2) -> rule6) triple2) -> rule1)) -> rule3))]
("Charlie" "is" "nice" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((((triple2) -> (rule5 % int4)) triple2) -> (rule6 % int3)) triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Charlie is not nice.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule4) OR ((((((((triple2) -> rule5) triple2) -> rule6) triple2) -> rule1)) -> rule3))]
("Charlie" "is" "nice" "-")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((((triple2) -> (rule5 % int4)) triple2) -> (rule6 % int3)) triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "smart" "-")
Fiona is young.
Unknown
rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "smart" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "green" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Charlie is blue.[(triple2)] Dave is green.[(triple3)] Fiona is nice.[(triple4)] @1: Anne is smart.[(((triple1) -> rule5))] Charlie is smart.[(((triple2) -> rule5))] Dave is nice.[(((triple3) -> rule3))] @2: Anne is young.[(((((triple1) -> rule5)) -> rule2))] Charlie is quiet.[(((((triple2) -> rule5) triple2) -> rule6))] Charlie is young.[(((((triple2) -> rule5)) -> rule2))] @3: Anne is nice.[(((((((triple1) -> rule5)) -> rule2)) -> rule4))] Charlie is green.[(((((((triple2) -> rule5) triple2) -> rule6) triple2) -> rule1))] Charlie is nice.[(((((((triple2) -> rule5)) -> rule2)) -> rule4) OR ((((((((triple2) -> rule5) triple2) -> rule6) triple2) -> rule1)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple2) -> (rule5 % int3)) triple2) -> (rule6 % int2)) triple2) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((((triple2) -> (rule5 % int4)) triple2) -> (rule6 % int3)) triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4