Dave is nice. Dave is round. Erin is rough. Fiona is quiet. Fiona is young. Harry is green. Harry is not rough. If Dave is green then Dave is not round. All nice things are not quiet. If something is cold then it is nice. If something is green then it is cold. If something is cold and not quiet then it is not young. If something is green and not young then it is round. If something is quiet and rough then it is round.
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
If Dave is green then Dave is not round.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "round" "-"))
All nice things are not quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "-"))
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is cold and not quiet then it is not young.
((("something" "is" "cold" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "young" "-"))
If something is green and not young then it is round.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "is" "round" "+"))
If something is quiet and rough then it is round.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
Erin is rough.
True
1
proof
[(triple3)]
("Erin" "is" "rough" "+")
triple3
Dave is not round.
False
1
inv-proof
[(triple2)]
("Dave" "is" "round" "-")
triple2
Dave is not quiet.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "quiet" "-")
((triple1) -> (rule2 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is quiet.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Harry is nice.
True
3
proof
[(((((triple6) -> rule4)) -> rule3))]
("Harry" "is" "nice" "+")
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((((triple6) -> rule4)) -> rule3))]
("Harry" "is" "nice" "-")
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not quiet.
True
4
proof
[(((((((triple6) -> rule4)) -> rule3)) -> rule2))]
("Harry" "is" "quiet" "-")
((((((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is quiet.
False
4
inv-proof
[(((((((triple6) -> rule4)) -> rule3)) -> rule2))]
("Harry" "is" "quiet" "+")
((((((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not young.
True
7
proof
[(((((triple6) -> rule4) ((((((triple6) -> rule4)) -> rule3)) -> rule2)) -> rule5))]
("Harry" "is" "young" "-")
((((triple6) -> (rule4 % int4)) ((((((triple6) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is not quiet.
("Harry" "is" "quiet" "-")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is young.
False
7
inv-proof
[(((((triple6) -> rule4) ((((((triple6) -> rule4)) -> rule3)) -> rule2)) -> rule5))]
("Harry" "is" "young" "+")
((((triple6) -> (rule4 % int4)) ((((((triple6) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is not quiet.
("Harry" "is" "quiet" "-")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is round.
True
9
proof
[(((triple6 ((((triple6) -> rule4) ((((((triple6) -> rule4)) -> rule3)) -> rule2)) -> rule5)) -> rule6))]
("Harry" "is" "round" "+")
((triple6 ((((triple6) -> (rule4 % int5)) ((((((triple6) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not young.
("Harry" "is" "young" "-")
int2
Harry is not quiet.
("Harry" "is" "quiet" "-")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
Harry is not round.
False
9
inv-proof
[(((triple6 ((((triple6) -> rule4) ((((((triple6) -> rule4)) -> rule3)) -> rule2)) -> rule5)) -> rule6))]
("Harry" "is" "round" "-")
((triple6 ((((triple6) -> (rule4 % int5)) ((((((triple6) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not young.
("Harry" "is" "young" "-")
int2
Harry is not quiet.
("Harry" "is" "quiet" "-")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "cold" "-")
Fiona is nice.
Unknown
rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Fiona" "is" "nice" "+")
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "cold" "-")
Fiona is round.
Unknown
rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "round" "+")
Erin is not nice.
Unknown
inv-rconc
[@2: Erin is nice.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is round.
Unknown
rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "round" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Dave is nice.[(triple1)] Dave is round.[(triple2)] Erin is rough.[(triple3)] Fiona is quiet.[(triple4)] Fiona is young.[(triple5)] Harry is green.[(triple6)] Harry is not rough.[(triple7)] @1: Dave is not quiet.[(((triple1) -> rule2))] Harry is cold.[(((triple6) -> rule4))] @2: Harry is nice.[(((((triple6) -> rule4)) -> rule3))] @3: Harry is not quiet.[(((((((triple6) -> rule4)) -> rule3)) -> rule2))] @4: Harry is not young.[(((((triple6) -> rule4) ((((((triple6) -> rule4)) -> rule3)) -> rule2)) -> rule5))] @5: Harry is round.[(((triple6 ((((triple6) -> rule4) ((((((triple6) -> rule4)) -> rule3)) -> rule2)) -> rule5)) -> rule6))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
Fiona is young.
("Fiona" "is" "young" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is not rough.
("Harry" "is" "rough" "-")
triple7
Dave is not quiet.
("Dave" "is" "quiet" "-")
((triple1) -> (rule2 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple6) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not quiet.
("Harry" "is" "quiet" "-")
((((((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not young.
("Harry" "is" "young" "-")
((((triple6) -> (rule4 % int4)) ((((((triple6) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is not quiet.
("Harry" "is" "quiet" "-")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
((triple6 ((((triple6) -> (rule4 % int5)) ((((((triple6) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not young.
("Harry" "is" "young" "-")
int2
Harry is not quiet.
("Harry" "is" "quiet" "-")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5