Charlie is rough. Dave is big. Dave is blue. Dave is green. Erin is quiet. Erin is young. Fiona is quiet. If Fiona is rough then Fiona is kind. If Erin is young then Erin is kind. If something is kind then it is blue. If Charlie is kind and Charlie is blue then Charlie is not young. If something is blue and rough then it is quiet. If something is green and not young then it is big. If something is blue and young then it is big. If Erin is big and Erin is blue then Erin is rough. Rough, blue things are not green.
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If Fiona is rough then Fiona is kind.
((("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "kind" "+"))
If Erin is young then Erin is kind.
((("Erin" "is" "young" "+")) -> ("Erin" "is" "kind" "+"))
If something is kind then it is blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If Charlie is kind and Charlie is blue then Charlie is not young.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "young" "-"))
If something is blue and rough then it is quiet.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If something is green and not young then it is big.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "is" "big" "+"))
If something is blue and young then it is big.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If Erin is big and Erin is blue then Erin is rough.
((("Erin" "is" "big" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "rough" "+"))
Rough, blue things are not green.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "-"))
Dave is big.
True
1
proof
[(triple2)]
("Dave" "is" "big" "+")
triple2
Erin is not young.
False
1
inv-proof
[(triple6)]
("Erin" "is" "young" "-")
triple6
Erin is kind.
True
2
proof
[(((triple6) -> rule2))]
("Erin" "is" "kind" "+")
((triple6) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple6) -> rule2))]
("Erin" "is" "kind" "-")
((triple6) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
True
3
proof
[(((((triple6) -> rule2)) -> rule3))]
("Erin" "is" "blue" "+")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not blue.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule3))]
("Erin" "is" "blue" "-")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
True
5
proof
[(((((((triple6) -> rule2)) -> rule3) triple6) -> rule7))]
("Erin" "is" "big" "+")
((((((triple6) -> (rule2 % int3))) -> (rule3 % int2)) triple6) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not big.
False
5
inv-proof
[(((((((triple6) -> rule2)) -> rule3) triple6) -> rule7))]
("Erin" "is" "big" "-")
((((((triple6) -> (rule2 % int3))) -> (rule3 % int2)) triple6) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is rough.
True
9
proof
[(((((((((triple6) -> rule2)) -> rule3) triple6) -> rule7) ((((triple6) -> rule2)) -> rule3)) -> rule8))]
("Erin" "is" "rough" "+")
((((((((triple6) -> (rule2 % int4))) -> (rule3 % int3)) triple6) -> (rule7 % int2)) ((((triple6) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is not rough.
False
9
inv-proof
[(((((((((triple6) -> rule2)) -> rule3) triple6) -> rule7) ((((triple6) -> rule2)) -> rule3)) -> rule8))]
("Erin" "is" "rough" "-")
((((((((triple6) -> (rule2 % int4))) -> (rule3 % int3)) triple6) -> (rule7 % int2)) ((((triple6) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is not green.
True
13
proof
[(((((((((((triple6) -> rule2)) -> rule3) triple6) -> rule7) ((((triple6) -> rule2)) -> rule3)) -> rule8) ((((triple6) -> rule2)) -> rule3)) -> rule9))]
("Erin" "is" "green" "-")
((((((((((triple6) -> (rule2 % int5))) -> (rule3 % int4)) triple6) -> (rule7 % int3)) ((((triple6) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule8 % int2)) ((((triple6) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule9 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
int5
Erin is green.
False
13
inv-proof
[(((((((((((triple6) -> rule2)) -> rule3) triple6) -> rule7) ((((triple6) -> rule2)) -> rule3)) -> rule8) ((((triple6) -> rule2)) -> rule3)) -> rule9))]
("Erin" "is" "green" "+")
((((((((((triple6) -> (rule2 % int5))) -> (rule3 % int4)) triple6) -> (rule7 % int3)) ((((triple6) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule8 % int2)) ((((triple6) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule9 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
int5
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "blue" "-")
Fiona is blue.
Unknown
rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "blue" "+")
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "big" "-")
Fiona is kind.
Unknown
rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "kind" "+")
Charlie is not quiet.
Unknown
inv-rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "big" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Charlie is rough.[(triple1)] Dave is big.[(triple2)] Dave is blue.[(triple3)] Dave is green.[(triple4)] Erin is quiet.[(triple5 OR ((((((triple6) -> rule2)) -> rule3) ((((((((triple6) -> rule2)) -> rule3) triple6) -> rule7) ((((triple6) -> rule2)) -> rule3)) -> rule8)) -> rule5))] Erin is young.[(triple6)] Fiona is quiet.[(triple7)] @1: Erin is kind.[(((triple6) -> rule2))] @2: Erin is blue.[(((((triple6) -> rule2)) -> rule3))] @3: Erin is big.[(((((((triple6) -> rule2)) -> rule3) triple6) -> rule7))] @4: Erin is rough.[(((((((((triple6) -> rule2)) -> rule3) triple6) -> rule7) ((((triple6) -> rule2)) -> rule3)) -> rule8))] @5: Erin is not green.[(((((((((((triple6) -> rule2)) -> rule3) triple6) -> rule7) ((((triple6) -> rule2)) -> rule3)) -> rule8) ((((triple6) -> rule2)) -> rule3)) -> rule9))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
((((((triple6) -> (rule2 % int5))) -> (rule3 % int4)) ((((((((triple6) -> (rule2 % int5))) -> (rule3 % int4)) triple6) -> (rule7 % int3)) ((((triple6) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule8 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
int5
Erin is young.
("Erin" "is" "young" "+")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
((triple6) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((((triple6) -> (rule2 % int3))) -> (rule3 % int2)) triple6) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
((((((((triple6) -> (rule2 % int4))) -> (rule3 % int3)) triple6) -> (rule7 % int2)) ((((triple6) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is not green.
("Erin" "is" "green" "-")
((((((((((triple6) -> (rule2 % int5))) -> (rule3 % int4)) triple6) -> (rule7 % int3)) ((((triple6) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule8 % int2)) ((((triple6) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule9 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
int5