Dave is blue. Dave is nice. Erin is rough. Gary is not green. Gary is nice. Gary is rough. Harry is rough. Nice things are white. If Harry is white then Harry is nice. Nice, white things are rough. If something is red and green then it is round. If something is rough and red then it is round. If something is white and not rough then it is not red. Rough things are red. If Dave is rough and Dave is round then Dave is green.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If Harry is white then Harry is nice.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "nice" "+"))
Nice, white things are rough.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If something is red and green then it is round.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something is rough and red then it is round.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
If something is white and not rough then it is not red.
((("something" "is" "white" "+") ("something" "is" "rough" "~")) -> ("something" "is" "red" "-"))
Rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If Dave is rough and Dave is round then Dave is green.
((("Dave" "is" "rough" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "green" "+"))
Gary is rough.
True
1
proof
[(triple6 OR ((triple5 ((triple5) -> rule1)) -> rule3))]
("Gary" "is" "rough" "+")
triple6
((triple5 ((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
False
1
inv-proof
[(triple4)]
("Gary" "is" "green" "+")
triple4
Dave is white.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "white" "+")
((triple2) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple6) -> rule7) OR ((((triple5 ((triple5) -> rule1)) -> rule3)) -> rule7))]
("Gary" "is" "red" "-")
((triple6) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple5 ((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Erin is round.
True
4
proof
[(((triple3 ((triple3) -> rule7)) -> rule5))]
("Erin" "is" "round" "+")
((triple3 ((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Harry is not round.
False
4
inv-proof
[(((triple7 ((triple7) -> rule7)) -> rule5))]
("Harry" "is" "round" "-")
((triple7 ((triple7) -> (rule7 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Dave is red.
True
5
proof
[(((((triple2 ((triple2) -> rule1)) -> rule3)) -> rule7))]
("Dave" "is" "red" "+")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not red.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule1)) -> rule3)) -> rule7))]
("Dave" "is" "red" "-")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is round.
True
10
proof
[(((((triple2 ((triple2) -> rule1)) -> rule3) ((((triple2 ((triple2) -> rule1)) -> rule3)) -> rule7)) -> rule5))]
("Dave" "is" "round" "+")
((((triple2 ((triple2) -> (rule1 % int4))) -> (rule3 % int3)) ((((triple2 ((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is not round.
False
10
inv-proof
[(((((triple2 ((triple2) -> rule1)) -> rule3) ((((triple2 ((triple2) -> rule1)) -> rule3)) -> rule7)) -> rule5))]
("Dave" "is" "round" "-")
((((triple2 ((triple2) -> (rule1 % int4))) -> (rule3 % int3)) ((((triple2 ((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is green.
True
15
proof
[(((((triple2 ((triple2) -> rule1)) -> rule3) ((((triple2 ((triple2) -> rule1)) -> rule3) ((((triple2 ((triple2) -> rule1)) -> rule3)) -> rule7)) -> rule5)) -> rule8))]
("Dave" "is" "green" "+")
((((triple2 ((triple2) -> (rule1 % int5))) -> (rule3 % int4)) ((((triple2 ((triple2) -> (rule1 % int5))) -> (rule3 % int4)) ((((triple2 ((triple2) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
Dave is not green.
False
15
inv-proof
[(((((triple2 ((triple2) -> rule1)) -> rule3) ((((triple2 ((triple2) -> rule1)) -> rule3) ((((triple2 ((triple2) -> rule1)) -> rule3)) -> rule7)) -> rule5)) -> rule8))]
("Dave" "is" "green" "-")
((((triple2 ((triple2) -> (rule1 % int5))) -> (rule3 % int4)) ((((triple2 ((triple2) -> (rule1 % int5))) -> (rule3 % int4)) ((((triple2 ((triple2) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
Harry is not white.
Unknown
inv-rconc
[@2: Harry is white.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "white" "-")
Erin is white.
Unknown
rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "white" "+")
Harry is not nice.
Unknown
inv-rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Harry" "is" "nice" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Dave is blue.[(triple1)] Dave is nice.[(triple2)] Erin is rough.[(triple3)] Gary is nice.[(triple5)] Gary is not green.[(triple4)] Gary is rough.[(triple6 OR ((triple5 ((triple5) -> rule1)) -> rule3))] Harry is rough.[(triple7)] @1: Dave is white.[(((triple2) -> rule1))] Erin is red.[(((triple3) -> rule7))] Gary is red.[(((triple6) -> rule7) OR ((((triple5 ((triple5) -> rule1)) -> rule3)) -> rule7))] Gary is white.[(((triple5) -> rule1))] Harry is red.[(((triple7) -> rule7))] @2: Dave is rough.[(((triple2 ((triple2) -> rule1)) -> rule3))] Erin is round.[(((triple3 ((triple3) -> rule7)) -> rule5))] Gary is round.[(((triple6 ((triple6) -> rule7)) -> rule5) OR ((((triple5 ((triple5) -> rule1)) -> rule3) ((triple6) -> rule7)) -> rule5) OR ((triple6 ((((triple5 ((triple5) -> rule1)) -> rule3)) -> rule7)) -> rule5) OR ((((triple5 ((triple5) -> rule1)) -> rule3) ((((triple5 ((triple5) -> rule1)) -> rule3)) -> rule7)) -> rule5))] Harry is round.[(((triple7 ((triple7) -> rule7)) -> rule5))] @3: Dave is red.[(((((triple2 ((triple2) -> rule1)) -> rule3)) -> rule7))] @4: Dave is round.[(((((triple2 ((triple2) -> rule1)) -> rule3) ((((triple2 ((triple2) -> rule1)) -> rule3)) -> rule7)) -> rule5))] @5: Dave is green.[(((((triple2 ((triple2) -> rule1)) -> rule3) ((((triple2 ((triple2) -> rule1)) -> rule3) ((((triple2 ((triple2) -> rule1)) -> rule3)) -> rule7)) -> rule5)) -> rule8))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Gary is not green.
("Gary" "is" "green" "-")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple6
((triple5 ((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
((triple2) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple3) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple6) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple5 ((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((triple5) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple7) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((triple3 ((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple6 ((triple6) -> (rule7 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple5 ((triple5) -> (rule1 % int4))) -> (rule3 % int3)) ((triple6) -> (rule7 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
((triple6 ((((triple5 ((triple5) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
((((triple5 ((triple5) -> (rule1 % int4))) -> (rule3 % int3)) ((((triple5 ((triple5) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
((triple7 ((triple7) -> (rule7 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((((triple2 ((triple2) -> (rule1 % int4))) -> (rule3 % int3)) ((((triple2 ((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
((((triple2 ((triple2) -> (rule1 % int5))) -> (rule3 % int4)) ((((triple2 ((triple2) -> (rule1 % int5))) -> (rule3 % int4)) ((((triple2 ((triple2) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5