Anne is quiet. Bob is blue. Erin is blue. Erin is smart. Erin is white. Harry is smart. Harry is white. If something is blue then it is nice. All green things are blue. Nice, white things are rough. All smart things are green. If something is nice then it is smart. Smart, green things are white.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is blue then it is nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Nice, white things are rough.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Smart, green things are white.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Erin is not blue.
False
1
inv-proof
[(triple3 OR ((((triple4) -> rule4)) -> rule2))]
("Erin" "is" "blue" "-")
triple3
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Anne is not green.
Unknown
inv-rconc
[@4: Anne is green.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule1 <- rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Anne is quiet.[(triple1)] Bob is blue.[(triple2)] Erin is blue.[(triple3 OR ((((triple4) -> rule4)) -> rule2))] Erin is smart.[(triple4 OR ((((triple3) -> rule1)) -> rule5))] Erin is white.[(triple5 OR ((triple4 ((triple4) -> rule4)) -> rule6) OR ((((((triple3) -> rule1)) -> rule5) ((triple4) -> rule4)) -> rule6) OR ((triple4 ((((((triple3) -> rule1)) -> rule5)) -> rule4)) -> rule6) OR ((((((triple3) -> rule1)) -> rule5) ((((((triple3) -> rule1)) -> rule5)) -> rule4)) -> rule6))] Harry is smart.[(triple6)] Harry is white.[(triple7 OR ((triple6 ((triple6) -> rule4)) -> rule6))] @1: Bob is nice.[(((triple2) -> rule1))] Erin is green.[(((triple4) -> rule4) OR ((((((triple3) -> rule1)) -> rule5)) -> rule4))] Erin is nice.[(((triple3) -> rule1) OR ((((((triple4) -> rule4)) -> rule2)) -> rule1))] Harry is green.[(((triple6) -> rule4))] @2: Bob is smart.[(((((triple2) -> rule1)) -> rule5))] Erin is rough.[(((((triple3) -> rule1) triple5) -> rule3) OR ((((triple3) -> rule1) ((triple4 ((triple4) -> rule4)) -> rule6)) -> rule3) OR ((((((((triple4) -> rule4)) -> rule2)) -> rule1) triple5) -> rule3) OR ((((triple3) -> rule1) ((((((triple3) -> rule1)) -> rule5) ((triple4) -> rule4)) -> rule6)) -> rule3) OR ((((((((triple4) -> rule4)) -> rule2)) -> rule1) ((triple4 ((triple4) -> rule4)) -> rule6)) -> rule3) OR ((((((((triple4) -> rule4)) -> rule2)) -> rule1) ((((((triple3) -> rule1)) -> rule5) ((triple4) -> rule4)) -> rule6)) -> rule3) OR ((((triple3) -> rule1) ((triple4 ((((((triple3) -> rule1)) -> rule5)) -> rule4)) -> rule6)) -> rule3) OR ((((triple3) -> rule1) ((((((triple3) -> rule1)) -> rule5) ((((((triple3) -> rule1)) -> rule5)) -> rule4)) -> rule6)) -> rule3) OR ((((((((triple4) -> rule4)) -> rule2)) -> rule1) ((triple4 ((((((triple3) -> rule1)) -> rule5)) -> rule4)) -> rule6)) -> rule3) OR ((((((((triple4) -> rule4)) -> rule2)) -> rule1) ((((((triple3) -> rule1)) -> rule5) ((((((triple3) -> rule1)) -> rule5)) -> rule4)) -> rule6)) -> rule3))] Harry is blue.[(((((triple6) -> rule4)) -> rule2))] @3: Bob is green.[(((((((triple2) -> rule1)) -> rule5)) -> rule4))] Harry is nice.[(((((((triple6) -> rule4)) -> rule2)) -> rule1))] @4: Bob is white.[(((((((triple2) -> rule1)) -> rule5) ((((((triple2) -> rule1)) -> rule5)) -> rule4)) -> rule6))] Harry is rough.[(((((((((triple6) -> rule4)) -> rule2)) -> rule1) triple7) -> rule3) OR ((((((((triple6) -> rule4)) -> rule2)) -> rule1) ((triple6 ((triple6) -> rule4)) -> rule6)) -> rule3))] @5: Bob is rough.[(((((triple2) -> rule1) ((((((triple2) -> rule1)) -> rule5) ((((((triple2) -> rule1)) -> rule5)) -> rule4)) -> rule6)) -> rule3))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple4
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple5
((triple4 ((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((((triple3) -> (rule1 % int4))) -> (rule5 % int3)) ((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
((triple4 ((((((triple3) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
((((((triple3) -> (rule1 % int4))) -> (rule5 % int3)) ((((((triple3) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Harry is smart.
("Harry" "is" "smart" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
((triple6 ((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple4) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((((triple4) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((triple6) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple3) -> (rule1 % int4)) ((triple4 ((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
((((((((triple4) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
((((triple3) -> (rule1 % int5)) ((((((triple3) -> (rule1 % int5))) -> (rule5 % int4)) ((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
int5
((((((((triple4) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule1 % int3)) ((triple4 ((triple4) -> (rule4 % int5))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5
((((((((triple4) -> (rule4 % int6))) -> (rule2 % int5))) -> (rule1 % int4)) ((((((triple3) -> (rule1 % int4))) -> (rule5 % int3)) ((triple4) -> (rule4 % int6))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5
Erin is green.
("Erin" "is" "green" "+")
int6
((((triple3) -> (rule1 % int5)) ((triple4 ((((((triple3) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
int5
((((triple3) -> (rule1 % int5)) ((((((triple3) -> (rule1 % int5))) -> (rule5 % int4)) ((((((triple3) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
int5
((((((((triple4) -> (rule4 % int6))) -> (rule2 % int5))) -> (rule1 % int4)) ((triple4 ((((((triple3) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int6))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5
Erin is green.
("Erin" "is" "green" "+")
int6
((((((((triple4) -> (rule4 % int6))) -> (rule2 % int5))) -> (rule1 % int4)) ((((((triple3) -> (rule1 % int4))) -> (rule5 % int3)) ((((((triple3) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int6))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5
Erin is green.
("Erin" "is" "green" "+")
int6
Harry is blue.
("Harry" "is" "blue" "+")
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((((((triple2) -> (rule1 % int4))) -> (rule5 % int3)) ((((((triple2) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
((((((((triple6) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
((((((((triple6) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule1 % int3)) ((triple6 ((triple6) -> (rule4 % int5))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
int5
Bob is rough.
("Bob" "is" "rough" "+")
((((triple2) -> (rule1 % int5)) ((((((triple2) -> (rule1 % int5))) -> (rule5 % int4)) ((((((triple2) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
int5