Charlie is round. Dave is green. Dave is kind. Dave is quiet. Dave is round. Dave is young. Fiona is not kind. Fiona is rough. Fiona is young. Harry is young. Kind, round things are rough. If Dave is round then Dave is quiet. Kind, young things are quiet. Round things are kind. If Charlie is rough and Charlie is kind then Charlie is cold. If something is cold and quiet then it is green. If something is rough and not quiet then it is green. If something is round then it is green.
Charlie is round.
("Charlie" "is" "round" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is not kind.
("Fiona" "is" "kind" "-")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is young.
("Harry" "is" "young" "+")
Kind, round things are rough.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If Dave is round then Dave is quiet.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "quiet" "+"))
Kind, young things are quiet.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If Charlie is rough and Charlie is kind then Charlie is cold.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "cold" "+"))
If something is cold and quiet then it is green.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is rough and not quiet then it is green.
((("something" "is" "rough" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "green" "+"))
If something is round then it is green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Dave is quiet.
True
1
proof
[(triple4 OR ((triple5) -> rule2) OR ((triple3 triple6) -> rule3) OR ((((triple5) -> rule4) triple6) -> rule3))]
("Dave" "is" "quiet" "+")
triple4
((triple5) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple3 triple6) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple5) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not quiet.
False
1
inv-proof
[(triple4 OR ((triple5) -> rule2) OR ((triple3 triple6) -> rule3) OR ((((triple5) -> rule4) triple6) -> rule3))]
("Dave" "is" "quiet" "-")
triple4
((triple5) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple3 triple6) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple5) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Charlie is kind.
True
2
proof
[(((triple1) -> rule4))]
("Charlie" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple1) -> rule4))]
("Charlie" "is" "kind" "-")
((triple1) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
True
4
proof
[(((((triple1) -> rule4) triple1) -> rule1))]
("Charlie" "is" "rough" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not rough.
False
4
inv-proof
[(((((triple1) -> rule4) triple1) -> rule1))]
("Charlie" "is" "rough" "-")
((((triple1) -> (rule4 % int2)) triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
True
7
proof
[(((((((triple1) -> rule4) triple1) -> rule1) ((triple1) -> rule4)) -> rule5))]
("Charlie" "is" "cold" "+")
((((((triple1) -> (rule4 % int3)) triple1) -> (rule1 % int2)) ((triple1) -> (rule4 % int3))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not cold.
False
7
inv-proof
[(((((((triple1) -> rule4) triple1) -> rule1) ((triple1) -> rule4)) -> rule5))]
("Charlie" "is" "cold" "-")
((((((triple1) -> (rule4 % int3)) triple1) -> (rule1 % int2)) ((triple1) -> (rule4 % int3))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "green" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "green" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Charlie is round.[(triple1)] Dave is green.[(triple2 OR ((triple5) -> rule8))] Dave is kind.[(triple3 OR ((triple5) -> rule4))] Dave is quiet.[(triple4 OR ((triple5) -> rule2) OR ((triple3 triple6) -> rule3) OR ((((triple5) -> rule4) triple6) -> rule3))] Dave is round.[(triple5)] Dave is young.[(triple6)] Fiona is not kind.[(triple7)] Fiona is rough.[(triple8)] Fiona is young.[(triple9)] Harry is young.[(triple10)] @1: Charlie is green.[(((triple1) -> rule8))] Charlie is kind.[(((triple1) -> rule4))] Dave is rough.[(((triple3 triple5) -> rule1) OR ((((triple5) -> rule4) triple5) -> rule1))] @2: Charlie is rough.[(((((triple1) -> rule4) triple1) -> rule1))] @3: Charlie is cold.[(((((((triple1) -> rule4) triple1) -> rule1) ((triple1) -> rule4)) -> rule5))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
((triple5) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple3
((triple5) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
((triple5) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple3 triple6) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple5) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple7
Fiona is rough.
("Fiona" "is" "rough" "+")
triple8
Fiona is young.
("Fiona" "is" "young" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple3 triple5) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple5) -> (rule4 % int2)) triple5) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple1) -> (rule4 % int3)) triple1) -> (rule1 % int2)) ((triple1) -> (rule4 % int3))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3