Charlie is kind. Charlie is rough. Erin is quiet. Fiona is kind. Harry is kind. Harry is quiet. Harry is young. All kind people are quiet. Cold people are not big. If Erin is quiet then Erin is cold. Green, cold people are not young. If Fiona is green and Fiona is quiet then Fiona is not young. Cold, kind people are rough. If someone is green and kind then they are rough. If someone is cold and not big then they are rough. If someone is rough then they are green.
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
All kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Cold people are not big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "-"))
If Erin is quiet then Erin is cold.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "cold" "+"))
Green, cold people are not young.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "-"))
If Fiona is green and Fiona is quiet then Fiona is not young.
((("Fiona" "is" "green" "+") ("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "young" "-"))
Cold, kind people are rough.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is green and kind then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold and not big then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "rough" "+"))
If someone is rough then they are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
Fiona is kind.
True
1
proof
[(triple4)]
("Fiona" "is" "kind" "+")
triple4
Erin is not quiet.
False
1
inv-proof
[(triple3)]
("Erin" "is" "quiet" "-")
triple3
Fiona is quiet.
True
2
proof
[(((triple4) -> rule1))]
("Fiona" "is" "quiet" "+")
((triple4) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is not quiet.
False
2
inv-proof
[(((triple4) -> rule1))]
("Fiona" "is" "quiet" "-")
((triple4) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Erin is not big.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("Erin" "is" "big" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is big.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("Erin" "is" "big" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
True
6
proof
[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule2)) -> rule8))]
("Erin" "is" "rough" "+")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not big.
("Erin" "is" "big" "-")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not rough.
False
6
inv-proof
[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule2)) -> rule8))]
("Erin" "is" "rough" "-")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not big.
("Erin" "is" "big" "-")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is green.
True
7
proof
[(((((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule2)) -> rule8)) -> rule9))]
("Erin" "is" "green" "+")
((((((triple3) -> (rule3 % int4)) ((((triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not big.
("Erin" "is" "big" "-")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is not green.
False
7
inv-proof
[(((((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule2)) -> rule8)) -> rule9))]
("Erin" "is" "green" "-")
((((((triple3) -> (rule3 % int4)) ((((triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not big.
("Erin" "is" "big" "-")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is not young.
True
10
proof
[(((((((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule2)) -> rule8)) -> rule9) ((triple3) -> rule3)) -> rule4))]
("Erin" "is" "young" "-")
((((((((triple3) -> (rule3 % int5)) ((((triple3) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2)) ((triple3) -> (rule3 % int5))) -> (rule4 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not big.
("Erin" "is" "big" "-")
int4
Erin is cold.
("Erin" "is" "cold" "+")
int5
Erin is young.
False
10
inv-proof
[(((((((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule2)) -> rule8)) -> rule9) ((triple3) -> rule3)) -> rule4))]
("Erin" "is" "young" "+")
((((((((triple3) -> (rule3 % int5)) ((((triple3) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2)) ((triple3) -> (rule3 % int5))) -> (rule4 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not big.
("Erin" "is" "big" "-")
int4
Erin is cold.
("Erin" "is" "cold" "+")
int5
Harry is not green.
Unknown
inv-rconc
[@2: Harry is green.[CWA. Example of deepest failure = (rule9 <- rule6 <- FAIL)]]
("Harry" "is" "green" "-")
Harry is rough.
Unknown
rconc
[@3: Harry is rough.[CWA. Example of deepest failure = (rule7 <- rule9 <- rule6 <- FAIL)]]
("Harry" "is" "rough" "+")
Fiona is not rough.
Unknown
inv-rconc
[@3: Fiona is rough.[CWA. Example of deepest failure = (rule7 <- rule9 <- rule6 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is green.
Unknown
rconc
[@2: Fiona is green.[CWA. Example of deepest failure = (rule9 <- rule6 <- FAIL)]]
("Fiona" "is" "green" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is kind.[(triple1)] Charlie is rough.[(triple2)] Erin is quiet.[(triple3)] Fiona is kind.[(triple4)] Harry is kind.[(triple5)] Harry is quiet.[(triple6 OR ((triple5) -> rule1))] Harry is young.[(triple7)] @1: Charlie is green.[(((triple2) -> rule9))] Charlie is quiet.[(((triple1) -> rule1))] Erin is cold.[(((triple3) -> rule3))] Fiona is quiet.[(((triple4) -> rule1))] @2: Erin is not big.[(((((triple3) -> rule3)) -> rule2))] @3: Erin is rough.[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule2)) -> rule8))] @4: Erin is green.[(((((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule2)) -> rule8)) -> rule9))] @5: Erin is not young.[(((((((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule2)) -> rule8)) -> rule9) ((triple3) -> rule3)) -> rule4))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Fiona is kind.
("Fiona" "is" "kind" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
((triple5) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple2) -> (rule9 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple4) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Erin is not big.
("Erin" "is" "big" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not big.
("Erin" "is" "big" "-")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((((((triple3) -> (rule3 % int4)) ((((triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not big.
("Erin" "is" "big" "-")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is not young.
("Erin" "is" "young" "-")
((((((((triple3) -> (rule3 % int5)) ((((triple3) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2)) ((triple3) -> (rule3 % int5))) -> (rule4 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not big.
("Erin" "is" "big" "-")
int4
Erin is cold.
("Erin" "is" "cold" "+")
int5