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