Dave is quiet. Dave is round. Erin is quiet. Erin is round. Erin is young. Fiona is cold. Harry is quiet. All nice, quiet people are rough. All quiet people are nice. If someone is white and rough then they are round. All round, rough people are cold. Quiet, cold people are white. Quiet, rough people are cold.
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All nice, quiet people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If someone is white and rough then they are round.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
All round, rough people are cold.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Quiet, cold people are white.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Quiet, rough people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Dave is round.
True
1
proof
[(triple2 OR ((((triple1 ((triple1 ((((triple1) -> rule2) triple1) -> rule1)) -> rule6)) -> rule5) ((((triple1) -> rule2) triple1) -> rule1)) -> rule3))]
("Dave" "is" "round" "+")
triple2
((((triple1 ((triple1 ((((triple1) -> (rule2 % int5)) triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((((triple1) -> (rule2 % int5)) triple1) -> (rule1 % int4))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Erin is not young.
False
1
inv-proof
[(triple5)]
("Erin" "is" "young" "-")
triple5
Erin is nice.
True
2
proof
[(((triple3) -> rule2))]
("Erin" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple7) -> rule2))]
("Harry" "is" "nice" "-")
((triple7) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Dave is rough.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule1))]
("Dave" "is" "rough" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Erin is not rough.
False
4
inv-proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("Erin" "is" "rough" "-")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Harry is cold.
True
6
proof
[(((triple7 ((((triple7) -> rule2) triple7) -> rule1)) -> rule6))]
("Harry" "is" "cold" "+")
((triple7 ((((triple7) -> (rule2 % int3)) triple7) -> (rule1 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Erin is not cold.
False
6
inv-proof
[(((triple3 ((((triple3) -> rule2) triple3) -> rule1)) -> rule6) OR ((triple4 ((((triple3) -> rule2) triple3) -> rule1)) -> rule4))]
("Erin" "is" "cold" "-")
((triple3 ((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
((triple4 ((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is white.
True
8
proof
[(((triple3 ((triple3 ((((triple3) -> rule2) triple3) -> rule1)) -> rule6)) -> rule5) OR ((triple3 ((triple4 ((((triple3) -> rule2) triple3) -> rule1)) -> rule4)) -> rule5))]
("Erin" "is" "white" "+")
((triple3 ((triple3 ((((triple3) -> (rule2 % int4)) triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
((triple3 ((triple4 ((((triple3) -> (rule2 % int4)) triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Dave is not white.
False
8
inv-proof
[(((triple1 ((triple1 ((((triple1) -> rule2) triple1) -> rule1)) -> rule6)) -> rule5) OR ((triple1 ((triple2 ((((triple1) -> rule2) triple1) -> rule1)) -> rule4)) -> rule5))]
("Dave" "is" "white" "-")
((triple1 ((triple1 ((((triple1) -> (rule2 % int4)) triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
((triple1 ((triple2 ((((triple1) -> (rule2 % int4)) triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Harry is round.
True
13
proof
[(((((triple7 ((triple7 ((((triple7) -> rule2) triple7) -> rule1)) -> rule6)) -> rule5) ((((triple7) -> rule2) triple7) -> rule1)) -> rule3))]
("Harry" "is" "round" "+")
((((triple7 ((triple7 ((((triple7) -> (rule2 % int5)) triple7) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((((triple7) -> (rule2 % int5)) triple7) -> (rule1 % int4))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
int5
Harry is not round.
False
13
inv-proof
[(((((triple7 ((triple7 ((((triple7) -> rule2) triple7) -> rule1)) -> rule6)) -> rule5) ((((triple7) -> rule2) triple7) -> rule1)) -> rule3))]
("Harry" "is" "round" "-")
((((triple7 ((triple7 ((((triple7) -> (rule2 % int5)) triple7) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((((triple7) -> (rule2 % int5)) triple7) -> (rule1 % int4))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
int5
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "white" "-")
Fiona is round.
Unknown
rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Fiona" "is" "round" "+")
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is rough.
Unknown
rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "rough" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Dave is quiet.[(triple1)] Dave is round.[(triple2 OR ((((triple1 ((triple1 ((((triple1) -> rule2) triple1) -> rule1)) -> rule6)) -> rule5) ((((triple1) -> rule2) triple1) -> rule1)) -> rule3))] Erin is quiet.[(triple3)] Erin is round.[(triple4 OR ((((triple3 ((triple3 ((((triple3) -> rule2) triple3) -> rule1)) -> rule6)) -> rule5) ((((triple3) -> rule2) triple3) -> rule1)) -> rule3))] Erin is young.[(triple5)] Fiona is cold.[(triple6)] Harry is quiet.[(triple7)] @1: Dave is nice.[(((triple1) -> rule2))] Erin is nice.[(((triple3) -> rule2))] Harry is nice.[(((triple7) -> rule2))] @2: Dave is rough.[(((((triple1) -> rule2) triple1) -> rule1))] Erin is rough.[(((((triple3) -> rule2) triple3) -> rule1))] Harry is rough.[(((((triple7) -> rule2) triple7) -> rule1))] @3: Dave is cold.[(((triple1 ((((triple1) -> rule2) triple1) -> rule1)) -> rule6) OR ((triple2 ((((triple1) -> rule2) triple1) -> rule1)) -> rule4))] Erin is cold.[(((triple3 ((((triple3) -> rule2) triple3) -> rule1)) -> rule6) OR ((triple4 ((((triple3) -> rule2) triple3) -> rule1)) -> rule4))] Harry is cold.[(((triple7 ((((triple7) -> rule2) triple7) -> rule1)) -> rule6))] @4: Dave is white.[(((triple1 ((triple1 ((((triple1) -> rule2) triple1) -> rule1)) -> rule6)) -> rule5) OR ((triple1 ((triple2 ((((triple1) -> rule2) triple1) -> rule1)) -> rule4)) -> rule5))] Erin is white.[(((triple3 ((triple3 ((((triple3) -> rule2) triple3) -> rule1)) -> rule6)) -> rule5) OR ((triple3 ((triple4 ((((triple3) -> rule2) triple3) -> rule1)) -> rule4)) -> rule5))] Harry is white.[(((triple7 ((triple7 ((((triple7) -> rule2) triple7) -> rule1)) -> rule6)) -> rule5))] @5: Harry is round.[(((((triple7 ((triple7 ((((triple7) -> rule2) triple7) -> rule1)) -> rule6)) -> rule5) ((((triple7) -> rule2) triple7) -> rule1)) -> rule3))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
((((triple1 ((triple1 ((((triple1) -> (rule2 % int5)) triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((((triple1) -> (rule2 % int5)) triple1) -> (rule1 % int4))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
triple4
((((triple3 ((triple3 ((((triple3) -> (rule2 % int5)) triple3) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((((triple3) -> (rule2 % int5)) triple3) -> (rule1 % int4))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
int5
Erin is young.
("Erin" "is" "young" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple7) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple7) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((triple1 ((((triple1) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((triple2 ((((triple1) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((triple3 ((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
((triple4 ((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
((triple7 ((((triple7) -> (rule2 % int3)) triple7) -> (rule1 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((triple1 ((triple1 ((((triple1) -> (rule2 % int4)) triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
((triple1 ((triple2 ((((triple1) -> (rule2 % int4)) triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
((triple3 ((triple3 ((((triple3) -> (rule2 % int4)) triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
((triple3 ((triple4 ((((triple3) -> (rule2 % int4)) triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
((triple7 ((triple7 ((((triple7) -> (rule2 % int4)) triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
((((triple7 ((triple7 ((((triple7) -> (rule2 % int5)) triple7) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((((triple7) -> (rule2 % int5)) triple7) -> (rule1 % int4))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
int5