Charlie is green. Charlie is kind. Charlie is nice. Charlie is round. Charlie is white. Dave is white. Erin is kind. Erin is round. Fiona is nice. Fiona is young. If Dave is green and Dave is round then Dave is nice. All nice things are kind. All round, white things are young. All young things are green. Big things are round. If something is white then it is round. Green, young things are white. If something is big and kind then it is young.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If Dave is green and Dave is round then Dave is nice.
((("Dave" "is" "green" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "nice" "+"))
All nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
All round, white things are young.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
All young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is white then it is round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Green, young things are white.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If something is big and kind then it is young.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Charlie is round.
True
1
proof
[(triple4 OR ((triple5) -> rule6))]
("Charlie" "is" "round" "+")
triple4
((triple5) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is not white.
False
1
inv-proof
[(triple6)]
("Dave" "is" "white" "-")
triple6
Dave is round.
True
2
proof
[(((triple6) -> rule6))]
("Dave" "is" "round" "+")
((triple6) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple6) -> rule6))]
("Dave" "is" "round" "-")
((triple6) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
True
4
proof
[(((((triple6) -> rule6) triple6) -> rule3))]
("Dave" "is" "young" "+")
((((triple6) -> (rule6 % int2)) triple6) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not young.
False
4
inv-proof
[(((((triple6) -> rule6) triple6) -> rule3))]
("Dave" "is" "young" "-")
((((triple6) -> (rule6 % int2)) triple6) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Fiona is round.
True
5
proof
[(((((((triple10) -> rule4) triple10) -> rule7)) -> rule6))]
("Fiona" "is" "round" "+")
((((((triple10) -> (rule4 % int3)) triple10) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Dave is not green.
False
5
inv-proof
[(((((((triple6) -> rule6) triple6) -> rule3)) -> rule4))]
("Dave" "is" "green" "-")
((((((triple6) -> (rule6 % int3)) triple6) -> (rule3 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is nice.
True
8
proof
[(((((((((triple6) -> rule6) triple6) -> rule3)) -> rule4) ((triple6) -> rule6)) -> rule1))]
("Dave" "is" "nice" "+")
((((((((triple6) -> (rule6 % int4)) triple6) -> (rule3 % int3))) -> (rule4 % int2)) ((triple6) -> (rule6 % int4))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is not nice.
False
8
inv-proof
[(((((((((triple6) -> rule6) triple6) -> rule3)) -> rule4) ((triple6) -> rule6)) -> rule1))]
("Dave" "is" "nice" "-")
((((((((triple6) -> (rule6 % int4)) triple6) -> (rule3 % int3))) -> (rule4 % int2)) ((triple6) -> (rule6 % int4))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is kind.
True
9
proof
[(((((((((((triple6) -> rule6) triple6) -> rule3)) -> rule4) ((triple6) -> rule6)) -> rule1)) -> rule2))]
("Dave" "is" "kind" "+")
((((((((((triple6) -> (rule6 % int5)) triple6) -> (rule3 % int4))) -> (rule4 % int3)) ((triple6) -> (rule6 % int5))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5
Dave is not kind.
False
9
inv-proof
[(((((((((((triple6) -> rule6) triple6) -> rule3)) -> rule4) ((triple6) -> rule6)) -> rule1)) -> rule2))]
("Dave" "is" "kind" "-")
((((((((((triple6) -> (rule6 % int5)) triple6) -> (rule3 % int4))) -> (rule4 % int3)) ((triple6) -> (rule6 % int5))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5
Erin is not young.
Unknown
inv-rconc
[@3: Erin is young.[CWA. Example of deepest failure = (rule3 <- rule7 <- rule8 <- FAIL)]]
("Erin" "is" "young" "-")
Erin is white.
Unknown
rconc
[@2: Erin is white.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Erin" "is" "white" "+")
Erin is not green.
Unknown
inv-rconc
[@3: Erin is green.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule7 <- FAIL)]]
("Erin" "is" "green" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Charlie is green.[(triple1 OR ((((triple4 triple5) -> rule3)) -> rule4) OR ((((((triple5) -> rule6) triple5) -> rule3)) -> rule4))] Charlie is kind.[(triple2 OR ((triple3) -> rule2))] Charlie is nice.[(triple3)] Charlie is round.[(triple4 OR ((triple5) -> rule6))] Charlie is white.[(triple5)] Dave is white.[(triple6)] Erin is kind.[(triple7)] Erin is round.[(triple8)] Fiona is nice.[(triple9)] Fiona is young.[(triple10)] @1: Charlie is young.[(((triple4 triple5) -> rule3) OR ((((triple5) -> rule6) triple5) -> rule3))] Dave is round.[(((triple6) -> rule6))] Fiona is green.[(((triple10) -> rule4))] Fiona is kind.[(((triple9) -> rule2))] @2: Dave is young.[(((((triple6) -> rule6) triple6) -> rule3))] Fiona is white.[(((((triple10) -> rule4) triple10) -> rule7))] @3: Dave is green.[(((((((triple6) -> rule6) triple6) -> rule3)) -> rule4))] Fiona is round.[(((((((triple10) -> rule4) triple10) -> rule7)) -> rule6))] @4: Dave is nice.[(((((((((triple6) -> rule6) triple6) -> rule3)) -> rule4) ((triple6) -> rule6)) -> rule1))] @5: Dave is kind.[(((((((((((triple6) -> rule6) triple6) -> rule3)) -> rule4) ((triple6) -> rule6)) -> rule1)) -> rule2))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
((((triple4 triple5) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((((triple5) -> (rule6 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
((triple5) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is round.
("Erin" "is" "round" "+")
triple8
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
Fiona is young.
("Fiona" "is" "young" "+")
triple10
Charlie is young.
("Charlie" "is" "young" "+")
((triple4 triple5) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple5) -> (rule6 % int2)) triple5) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((triple6) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple10) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple9) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple6) -> (rule6 % int2)) triple6) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple10) -> (rule4 % int2)) triple10) -> (rule7 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((((triple6) -> (rule6 % int3)) triple6) -> (rule3 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
((((((triple10) -> (rule4 % int3)) triple10) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((((((triple6) -> (rule6 % int4)) triple6) -> (rule3 % int3))) -> (rule4 % int2)) ((triple6) -> (rule6 % int4))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
((((((((((triple6) -> (rule6 % int5)) triple6) -> (rule3 % int4))) -> (rule4 % int3)) ((triple6) -> (rule6 % int5))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5