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