Charlie is smart. Dave is green. Dave is red. Dave is round. Dave is smart. Erin is green. Erin is kind. Erin is not red. Erin is round. Erin is young. Harry is green. Harry is kind. All kind, round things are white. If something is red then it is white. If Charlie is kind then Charlie is round. All green, smart things are red. All smart things are green. White things are young.
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not red.
("Erin" "is" "red" "-")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All kind, round things are white.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If something is red then it is white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If Charlie is kind then Charlie is round.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "round" "+"))
All green, smart things are red.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
White things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
Harry is green.
True
1
proof
[(triple11)]
("Harry" "is" "green" "+")
triple11
Erin is not green.
False
1
inv-proof
[(triple6)]
("Erin" "is" "green" "-")
triple6
Erin is white.
True
3
proof
[(((triple7 triple9) -> rule1))]
("Erin" "is" "white" "+")
((triple7 triple9) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple1) -> rule5))]
("Charlie" "is" "green" "-")
((triple1) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
True
4
proof
[(((((triple1) -> rule5) triple1) -> rule4))]
("Charlie" "is" "red" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Dave is not young.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule6) OR ((((((triple2 triple5) -> rule4)) -> rule2)) -> rule6) OR ((((((((triple5) -> rule5) triple5) -> rule4)) -> rule2)) -> rule6))]
("Dave" "is" "young" "-")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple2 triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((((triple5) -> (rule5 % int4)) triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Charlie is white.
True
5
proof
[(((((((triple1) -> rule5) triple1) -> rule4)) -> rule2))]
("Charlie" "is" "white" "+")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is not white.
False
5
inv-proof
[(((((((triple1) -> rule5) triple1) -> rule4)) -> rule2))]
("Charlie" "is" "white" "-")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is white.
Unknown
rconc
[@2: Harry is white.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Harry" "is" "white" "+")
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "round" "-")
Harry is young.
Unknown
rconc
[@3: Harry is young.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule4 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Charlie is smart.[(triple1)] Dave is green.[(triple2 OR ((triple5) -> rule5))] Dave is red.[(triple3 OR ((triple2 triple5) -> rule4) OR ((((triple5) -> rule5) triple5) -> rule4))] Dave is round.[(triple4)] Dave is smart.[(triple5)] Erin is green.[(triple6)] Erin is kind.[(triple7)] Erin is not red.[(triple8)] Erin is round.[(triple9)] Erin is young.[(triple10 OR ((((triple7 triple9) -> rule1)) -> rule6))] Harry is green.[(triple11)] Harry is kind.[(triple12)] @1: Charlie is green.[(((triple1) -> rule5))] Dave is white.[(((triple3) -> rule2) OR ((((triple2 triple5) -> rule4)) -> rule2) OR ((((((triple5) -> rule5) triple5) -> rule4)) -> rule2))] Erin is white.[(((triple7 triple9) -> rule1))] @2: Charlie is red.[(((((triple1) -> rule5) triple1) -> rule4))] Dave is young.[(((((triple3) -> rule2)) -> rule6) OR ((((((triple2 triple5) -> rule4)) -> rule2)) -> rule6) OR ((((((((triple5) -> rule5) triple5) -> rule4)) -> rule2)) -> rule6))] @3: Charlie is white.[(((((((triple1) -> rule5) triple1) -> rule4)) -> rule2))] @4: Charlie is young.[(((((((((triple1) -> rule5) triple1) -> rule4)) -> rule2)) -> rule6))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
((triple5) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple3
((triple2 triple5) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple5) -> (rule5 % int2)) triple5) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is not red.
("Erin" "is" "red" "-")
triple8
Erin is round.
("Erin" "is" "round" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
((((triple7 triple9) -> (rule1 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is kind.
("Harry" "is" "kind" "+")
triple12
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple3) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple2 triple5) -> (rule4 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((((triple5) -> (rule5 % int3)) triple5) -> (rule4 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((triple7 triple9) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple2 triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((((triple5) -> (rule5 % int4)) triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
((((((((triple1) -> (rule5 % int4)) triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4