Dave is kind. Dave is quiet. Dave is red. Dave is rough. Dave is white. Erin is big. Fiona is green. Fiona is rough. Harry is kind. Harry is quiet. If Erin is green and Erin is big then Erin is rough. Quiet, big people are white. Quiet people are rough. All rough people are white. Kind, red people are green. All red, quiet people are rough. All big people are red. White, big people are rough. White people are big.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Erin is green and Erin is big then Erin is rough.
((("Erin" "is" "green" "+") ("Erin" "is" "big" "+")) -> ("Erin" "is" "rough" "+"))
Quiet, big people are white.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
All rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Kind, red people are green.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
All red, quiet people are rough.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
All big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
White, big people are rough.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
White people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Dave is kind.
True
1
proof
[(triple1)]
("Dave" "is" "kind" "+")
triple1
Dave is not rough.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule3) OR ((triple3 triple2) -> rule6) OR ((triple5 ((triple5) -> rule9)) -> rule8) OR ((((((triple5) -> rule9)) -> rule7) triple2) -> rule6))]
("Dave" "is" "rough" "-")
triple4
((triple2) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple3 triple2) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple5 ((triple5) -> (rule9 % int2))) -> (rule8 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((((triple5) -> (rule9 % int3))) -> (rule7 % int2)) triple2) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is green.
True
3
proof
[(((triple1 triple3) -> rule5) OR ((triple1 ((((triple5) -> rule9)) -> rule7)) -> rule5) OR ((triple1 ((((((triple4) -> rule4)) -> rule9)) -> rule7)) -> rule5) OR ((triple1 ((((((((triple2) -> rule3)) -> rule4)) -> rule9)) -> rule7)) -> rule5))]
("Dave" "is" "green" "+")
((triple1 triple3) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple1 ((((triple5) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((triple1 ((((((triple4) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((triple1 ((((((((triple2) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
Fiona is not white.
False
2
inv-proof
[(((triple8) -> rule4))]
("Fiona" "is" "white" "-")
((triple8) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
True
3
proof
[(((((triple8) -> rule4)) -> rule9))]
("Fiona" "is" "big" "+")
((((triple8) -> (rule4 % int2))) -> (rule9 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is not big.
False
3
inv-proof
[(((((triple8) -> rule4)) -> rule9))]
("Fiona" "is" "big" "-")
((((triple8) -> (rule4 % int2))) -> (rule9 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Harry is big.
True
4
proof
[(((((((triple10) -> rule3)) -> rule4)) -> rule9))]
("Harry" "is" "big" "+")
((((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Fiona is not red.
False
4
inv-proof
[(((((((triple8) -> rule4)) -> rule9)) -> rule7))]
("Fiona" "is" "red" "-")
((((((triple8) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Harry is red.
True
5
proof
[(((((((((triple10) -> rule3)) -> rule4)) -> rule9)) -> rule7))]
("Harry" "is" "red" "+")
((((((((triple10) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is not red.
False
5
inv-proof
[(((((((((triple10) -> rule3)) -> rule4)) -> rule9)) -> rule7))]
("Harry" "is" "red" "-")
((((((((triple10) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is green.
True
7
proof
[(((triple9 ((((((((triple10) -> rule3)) -> rule4)) -> rule9)) -> rule7)) -> rule5))]
("Harry" "is" "green" "+")
((triple9 ((((((((triple10) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5
Harry is not green.
False
7
inv-proof
[(((triple9 ((((((((triple10) -> rule3)) -> rule4)) -> rule9)) -> rule7)) -> rule5))]
("Harry" "is" "green" "-")
((triple9 ((((((((triple10) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5
Erin is not rough.
Unknown
inv-rconc
[@4: Erin is rough.[CWA. Example of deepest failure = (rule8 <- rule4 <- rule1 <- rule5 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is white.
Unknown
rconc
[@3: Erin is white.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule5 <- FAIL)]]
("Erin" "is" "white" "+")
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Dave is kind.[(triple1)] Dave is quiet.[(triple2)] Dave is red.[(triple3 OR ((((triple5) -> rule9)) -> rule7) OR ((((((triple4) -> rule4)) -> rule9)) -> rule7) OR ((((((((triple2) -> rule3)) -> rule4)) -> rule9)) -> rule7))] Dave is rough.[(triple4 OR ((triple2) -> rule3) OR ((triple3 triple2) -> rule6) OR ((triple5 ((triple5) -> rule9)) -> rule8) OR ((((((triple5) -> rule9)) -> rule7) triple2) -> rule6))] Dave is white.[(triple5 OR ((triple4) -> rule4) OR ((((triple2) -> rule3)) -> rule4) OR ((((triple3 triple2) -> rule6)) -> rule4))] Erin is big.[(triple6)] Fiona is green.[(triple7)] Fiona is rough.[(triple8)] Harry is kind.[(triple9)] Harry is quiet.[(triple10)] @1: Dave is big.[(((triple5) -> rule9) OR ((((triple4) -> rule4)) -> rule9) OR ((((((triple2) -> rule3)) -> rule4)) -> rule9) OR ((((((triple3 triple2) -> rule6)) -> rule4)) -> rule9))] Dave is green.[(((triple1 triple3) -> rule5) OR ((triple1 ((((triple5) -> rule9)) -> rule7)) -> rule5) OR ((triple1 ((((((triple4) -> rule4)) -> rule9)) -> rule7)) -> rule5) OR ((triple1 ((((((((triple2) -> rule3)) -> rule4)) -> rule9)) -> rule7)) -> rule5))] Erin is red.[(((triple6) -> rule7))] Fiona is white.[(((triple8) -> rule4))] Harry is rough.[(((triple10) -> rule3))] @2: Fiona is big.[(((((triple8) -> rule4)) -> rule9))] Harry is white.[(((((triple10) -> rule3)) -> rule4))] @3: Fiona is red.[(((((((triple8) -> rule4)) -> rule9)) -> rule7))] Harry is big.[(((((((triple10) -> rule3)) -> rule4)) -> rule9))] @4: Harry is red.[(((((((((triple10) -> rule3)) -> rule4)) -> rule9)) -> rule7))] @5: Harry is green.[(((triple9 ((((((((triple10) -> rule3)) -> rule4)) -> rule9)) -> rule7)) -> rule5))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
((((triple5) -> (rule9 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((((triple4) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((((triple2) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
triple4
((triple2) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple3 triple2) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple5 ((triple5) -> (rule9 % int2))) -> (rule8 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((((triple5) -> (rule9 % int3))) -> (rule7 % int2)) triple2) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
triple5
((triple4) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple3 triple2) -> (rule6 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
triple6
Fiona is green.
("Fiona" "is" "green" "+")
triple7
Fiona is rough.
("Fiona" "is" "rough" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Dave is big.
("Dave" "is" "big" "+")
((triple5) -> (rule9 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule9 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple3 triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((triple1 triple3) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple1 ((((triple5) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((triple1 ((((((triple4) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((triple1 ((((((((triple2) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
Erin is red.
("Erin" "is" "red" "+")
((triple6) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple8) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple10) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((((triple8) -> (rule4 % int2))) -> (rule9 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((((((triple8) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
((((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((((((triple10) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
((triple9 ((((((((triple10) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5