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