Anne is green. Anne is round. Anne is smart. Anne is white. Dave is not cold. Dave is not green. Dave is nice. Dave is white. Gary is nice. Harry is cold. Harry is green. Harry is nice. Harry is not rough. Harry is round. Harry is smart. Harry is white. Rough people are smart. If someone is rough and smart then they are round. Green people are cold. All nice, round people are cold. Nice, smart people are cold. If someone is white and rough then they are green. If Gary is white and Gary is nice then Gary is smart. Round, cold people are white. If Gary is nice then Gary is rough.
Anne is green.
("Anne" "is" "green" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is not green.
("Dave" "is" "green" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is rough and smart then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
All nice, round people are cold.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Nice, smart people are cold.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is white and rough then they are green.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If Gary is white and Gary is nice then Gary is smart.
((("Gary" "is" "white" "+") ("Gary" "is" "nice" "+")) -> ("Gary" "is" "smart" "+"))
Round, cold people are white.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If Gary is nice then Gary is rough.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "rough" "+"))
Harry is nice.
True
1
proof
[(triple12)]
("Harry" "is" "nice" "+")
triple12
Dave is not white.
False
1
inv-proof
[(triple8)]
("Dave" "is" "white" "-")
triple8
Anne is cold.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple9) -> rule9))]
("Gary" "is" "rough" "-")
((triple9) -> (rule9 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
True
3
proof
[(((((triple9) -> rule9)) -> rule1))]
("Gary" "is" "smart" "+")
((((triple9) -> (rule9 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((((triple9) -> rule9)) -> rule1))]
("Gary" "is" "smart" "-")
((((triple9) -> (rule9 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is round.
True
6
proof
[(((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2))]
("Gary" "is" "round" "+")
((((triple9) -> (rule9 % int3)) ((((triple9) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not cold.
False
5
inv-proof
[(((triple9 ((((triple9) -> rule9)) -> rule1)) -> rule5) OR ((triple9 ((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2)) -> rule4))]
("Gary" "is" "cold" "-")
((triple9 ((((triple9) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((triple9 ((((triple9) -> (rule9 % int4)) ((((triple9) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is white.
True
12
proof
[(((((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2) ((triple9 ((((triple9) -> rule9)) -> rule1)) -> rule5)) -> rule8) OR ((((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2) ((triple9 ((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2)) -> rule4)) -> rule8))]
("Gary" "is" "white" "+")
((((((triple9) -> (rule9 % int5)) ((((triple9) -> (rule9 % int5))) -> (rule1 % int4))) -> (rule2 % int3)) ((triple9 ((((triple9) -> (rule9 % int5))) -> (rule1 % int4))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5
((((((triple9) -> (rule9 % int5)) ((((triple9) -> (rule9 % int5))) -> (rule1 % int4))) -> (rule2 % int3)) ((triple9 ((((triple9) -> (rule9 % int5)) ((((triple9) -> (rule9 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5
Gary is not white.
False
12
inv-proof
[(((((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2) ((triple9 ((((triple9) -> rule9)) -> rule1)) -> rule5)) -> rule8) OR ((((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2) ((triple9 ((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2)) -> rule4)) -> rule8))]
("Gary" "is" "white" "-")
((((((triple9) -> (rule9 % int5)) ((((triple9) -> (rule9 % int5))) -> (rule1 % int4))) -> (rule2 % int3)) ((triple9 ((((triple9) -> (rule9 % int5))) -> (rule1 % int4))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5
((((((triple9) -> (rule9 % int5)) ((((triple9) -> (rule9 % int5))) -> (rule1 % int4))) -> (rule2 % int3)) ((triple9 ((((triple9) -> (rule9 % int5)) ((((triple9) -> (rule9 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5
Gary is green.
True
15
proof
[(((((((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2) ((triple9 ((((triple9) -> rule9)) -> rule1)) -> rule5)) -> rule8) ((triple9) -> rule9)) -> rule6) OR ((((((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2) ((triple9 ((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2)) -> rule4)) -> rule8) ((triple9) -> rule9)) -> rule6))]
("Gary" "is" "green" "+")
((((((((triple9) -> (rule9 % int6)) ((((triple9) -> (rule9 % int6))) -> (rule1 % int5))) -> (rule2 % int4)) ((triple9 ((((triple9) -> (rule9 % int6))) -> (rule1 % int5))) -> (rule5 % int3))) -> (rule8 % int2)) ((triple9) -> (rule9 % int6))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Gary is rough.
("Gary" "is" "rough" "+")
int6
((((((((triple9) -> (rule9 % int6)) ((((triple9) -> (rule9 % int6))) -> (rule1 % int5))) -> (rule2 % int4)) ((triple9 ((((triple9) -> (rule9 % int6)) ((((triple9) -> (rule9 % int6))) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) ((triple9) -> (rule9 % int6))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Gary is rough.
("Gary" "is" "rough" "+")
int6
Gary is not green.
False
15
inv-proof
[(((((((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2) ((triple9 ((((triple9) -> rule9)) -> rule1)) -> rule5)) -> rule8) ((triple9) -> rule9)) -> rule6) OR ((((((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2) ((triple9 ((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2)) -> rule4)) -> rule8) ((triple9) -> rule9)) -> rule6))]
("Gary" "is" "green" "-")
((((((((triple9) -> (rule9 % int6)) ((((triple9) -> (rule9 % int6))) -> (rule1 % int5))) -> (rule2 % int4)) ((triple9 ((((triple9) -> (rule9 % int6))) -> (rule1 % int5))) -> (rule5 % int3))) -> (rule8 % int2)) ((triple9) -> (rule9 % int6))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Gary is rough.
("Gary" "is" "rough" "+")
int6
((((((((triple9) -> (rule9 % int6)) ((((triple9) -> (rule9 % int6))) -> (rule1 % int5))) -> (rule2 % int4)) ((triple9 ((((triple9) -> (rule9 % int6)) ((((triple9) -> (rule9 % int6))) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) ((triple9) -> (rule9 % int6))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Gary is rough.
("Gary" "is" "rough" "+")
int6
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "round" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is green.[(triple1)] Anne is round.[(triple2)] Anne is smart.[(triple3)] Anne is white.[(triple4 OR ((triple2 ((triple1) -> rule3)) -> rule8))] Dave is nice.[(triple7)] Dave is not cold.[(triple5)] Dave is not green.[(triple6)] Dave is white.[(triple8)] Gary is nice.[(triple9)] Harry is cold.[(triple10 OR ((triple11) -> rule3) OR ((triple12 triple14) -> rule4) OR ((triple12 triple15) -> rule5))] Harry is green.[(triple11)] Harry is nice.[(triple12)] Harry is not rough.[(triple13)] Harry is round.[(triple14)] Harry is smart.[(triple15)] Harry is white.[(triple16 OR ((triple14 triple10) -> rule8) OR ((triple14 ((triple11) -> rule3)) -> rule8) OR ((triple14 ((triple12 triple14) -> rule4)) -> rule8) OR ((triple14 ((triple12 triple15) -> rule5)) -> rule8))] @1: Anne is cold.[(((triple1) -> rule3))] Gary is rough.[(((triple9) -> rule9))] @2: Gary is smart.[(((((triple9) -> rule9)) -> rule1))] @3: Gary is cold.[(((triple9 ((((triple9) -> rule9)) -> rule1)) -> rule5) OR ((triple9 ((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2)) -> rule4))] Gary is round.[(((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2))] @4: Gary is white.[(((((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2) ((triple9 ((((triple9) -> rule9)) -> rule1)) -> rule5)) -> rule8) OR ((((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2) ((triple9 ((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2)) -> rule4)) -> rule8))] @5: Gary is green.[(((((((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2) ((triple9 ((((triple9) -> rule9)) -> rule1)) -> rule5)) -> rule8) ((triple9) -> rule9)) -> rule6) OR ((((((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2) ((triple9 ((((triple9) -> rule9) ((((triple9) -> rule9)) -> rule1)) -> rule2)) -> rule4)) -> rule8) ((triple9) -> rule9)) -> rule6))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
((triple2 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Dave is not cold.
("Dave" "is" "cold" "-")
triple5
Dave is not green.
("Dave" "is" "green" "-")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
((triple11) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple12 triple14) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple12 triple15) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is nice.
("Harry" "is" "nice" "+")
triple12
Harry is not rough.
("Harry" "is" "rough" "-")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
((triple14 triple10) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple14 ((triple11) -> (rule3 % int2))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple14 ((triple12 triple14) -> (rule4 % int2))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple14 ((triple12 triple15) -> (rule5 % int2))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple9) -> (rule9 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((((triple9) -> (rule9 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((triple9 ((((triple9) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((triple9 ((((triple9) -> (rule9 % int4)) ((((triple9) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is round.
("Gary" "is" "round" "+")
((((triple9) -> (rule9 % int3)) ((((triple9) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((((((triple9) -> (rule9 % int5)) ((((triple9) -> (rule9 % int5))) -> (rule1 % int4))) -> (rule2 % int3)) ((triple9 ((((triple9) -> (rule9 % int5))) -> (rule1 % int4))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5
((((((triple9) -> (rule9 % int5)) ((((triple9) -> (rule9 % int5))) -> (rule1 % int4))) -> (rule2 % int3)) ((triple9 ((((triple9) -> (rule9 % int5)) ((((triple9) -> (rule9 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5
Gary is green.
("Gary" "is" "green" "+")
((((((((triple9) -> (rule9 % int6)) ((((triple9) -> (rule9 % int6))) -> (rule1 % int5))) -> (rule2 % int4)) ((triple9 ((((triple9) -> (rule9 % int6))) -> (rule1 % int5))) -> (rule5 % int3))) -> (rule8 % int2)) ((triple9) -> (rule9 % int6))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Gary is rough.
("Gary" "is" "rough" "+")
int6
((((((((triple9) -> (rule9 % int6)) ((((triple9) -> (rule9 % int6))) -> (rule1 % int5))) -> (rule2 % int4)) ((triple9 ((((triple9) -> (rule9 % int6)) ((((triple9) -> (rule9 % int6))) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) ((triple9) -> (rule9 % int6))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Gary is rough.
("Gary" "is" "rough" "+")
int6