Dave is young. Erin is smart. Fiona is not green. Fiona is not round. Fiona is smart. Fiona is not white. Gary is not blue. All young people are white. All white, young people are not blue. If someone is young and not blue then they are not quiet. Green people are smart. If someone is white and not quiet then they are green. If someone is smart and white then they are round.
Dave is young.
("Dave" "is" "young" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is not green.
("Fiona" "is" "green" "-")
Fiona is not round.
("Fiona" "is" "round" "-")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is not white.
("Fiona" "is" "white" "-")
Gary is not blue.
("Gary" "is" "blue" "-")
All young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
All white, young people are not blue.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "-"))
If someone is young and not blue then they are not quiet.
((("someone" "is" "young" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "quiet" "-"))
Green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
If someone is white and not quiet then they are green.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "green" "+"))
If someone is smart and white then they are round.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
Fiona is not white.
True
1
proof
[(triple6)]
("Fiona" "is" "white" "-")
triple6
Fiona is white.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "white" "+")
triple6
Dave is white.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "white" "+")
((triple1) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "white" "-")
((triple1) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not blue.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule2))]
("Dave" "is" "blue" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is blue.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule2))]
("Dave" "is" "blue" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not quiet.
True
6
proof
[(((triple1 ((((triple1) -> rule1) triple1) -> rule2)) -> rule3))]
("Dave" "is" "quiet" "-")
((triple1 ((((triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is quiet.
False
6
inv-proof
[(((triple1 ((((triple1) -> rule1) triple1) -> rule2)) -> rule3))]
("Dave" "is" "quiet" "+")
((triple1 ((((triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is green.
True
9
proof
[(((((triple1) -> rule1) ((triple1 ((((triple1) -> rule1) triple1) -> rule2)) -> rule3)) -> rule5))]
("Dave" "is" "green" "+")
((((triple1) -> (rule1 % int4)) ((triple1 ((((triple1) -> (rule1 % int4)) triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not quiet.
("Dave" "is" "quiet" "-")
int2
Dave is not blue.
("Dave" "is" "blue" "-")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is not green.
False
9
inv-proof
[(((((triple1) -> rule1) ((triple1 ((((triple1) -> rule1) triple1) -> rule2)) -> rule3)) -> rule5))]
("Dave" "is" "green" "-")
((((triple1) -> (rule1 % int4)) ((triple1 ((((triple1) -> (rule1 % int4)) triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not quiet.
("Dave" "is" "quiet" "-")
int2
Dave is not blue.
("Dave" "is" "blue" "-")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is smart.
True
10
proof
[(((((((triple1) -> rule1) ((triple1 ((((triple1) -> rule1) triple1) -> rule2)) -> rule3)) -> rule5)) -> rule4))]
("Dave" "is" "smart" "+")
((((((triple1) -> (rule1 % int5)) ((triple1 ((((triple1) -> (rule1 % int5)) triple1) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not quiet.
("Dave" "is" "quiet" "-")
int3
Dave is not blue.
("Dave" "is" "blue" "-")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
Dave is not smart.
False
10
inv-proof
[(((((((triple1) -> rule1) ((triple1 ((((triple1) -> rule1) triple1) -> rule2)) -> rule3)) -> rule5)) -> rule4))]
("Dave" "is" "smart" "-")
((((((triple1) -> (rule1 % int5)) ((triple1 ((((triple1) -> (rule1 % int5)) triple1) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not quiet.
("Dave" "is" "quiet" "-")
int3
Dave is not blue.
("Dave" "is" "blue" "-")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "green" "-")
Gary is round.
Unknown
rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Gary" "is" "round" "+")
Erin is not round.
Unknown
inv-rconc
[@2: Erin is round.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Erin" "is" "round" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "green" "+")
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "white" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "white" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Dave is young.[(triple1)] Erin is smart.[(triple2)] Fiona is not green.[(triple3)] Fiona is not round.[(triple4)] Fiona is not white.[(triple6)] Fiona is smart.[(triple5)] Gary is not blue.[(triple7)] @1: Dave is white.[(((triple1) -> rule1))] @2: Dave is not blue.[(((((triple1) -> rule1) triple1) -> rule2))] @3: Dave is not quiet.[(((triple1 ((((triple1) -> rule1) triple1) -> rule2)) -> rule3))] @4: Dave is green.[(((((triple1) -> rule1) ((triple1 ((((triple1) -> rule1) triple1) -> rule2)) -> rule3)) -> rule5))] @5: Dave is smart.[(((((((triple1) -> rule1) ((triple1 ((((triple1) -> rule1) triple1) -> rule2)) -> rule3)) -> rule5)) -> rule4))] @6: Dave is round.[(((((((((triple1) -> rule1) ((triple1 ((((triple1) -> rule1) triple1) -> rule2)) -> rule3)) -> rule5)) -> rule4) ((triple1) -> rule1)) -> rule6))]
Dave is young.
("Dave" "is" "young" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Fiona is not green.
("Fiona" "is" "green" "-")
triple3
Fiona is not round.
("Fiona" "is" "round" "-")
triple4
Fiona is not white.
("Fiona" "is" "white" "-")
triple6
Fiona is smart.
("Fiona" "is" "smart" "+")
triple5
Gary is not blue.
("Gary" "is" "blue" "-")
triple7
Dave is white.
("Dave" "is" "white" "+")
((triple1) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not quiet.
("Dave" "is" "quiet" "-")
((triple1 ((((triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((((triple1) -> (rule1 % int4)) ((triple1 ((((triple1) -> (rule1 % int4)) triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not quiet.
("Dave" "is" "quiet" "-")
int2
Dave is not blue.
("Dave" "is" "blue" "-")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple1) -> (rule1 % int5)) ((triple1 ((((triple1) -> (rule1 % int5)) triple1) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not quiet.
("Dave" "is" "quiet" "-")
int3
Dave is not blue.
("Dave" "is" "blue" "-")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
Dave is round.
("Dave" "is" "round" "+")
((((((((triple1) -> (rule1 % int6)) ((triple1 ((((triple1) -> (rule1 % int6)) triple1) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) ((triple1) -> (rule1 % int6))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not quiet.
("Dave" "is" "quiet" "-")
int4
Dave is not blue.
("Dave" "is" "blue" "-")
int5
Dave is white.
("Dave" "is" "white" "+")
int6