Charlie is quiet. Erin is cold. Erin is rough. Gary is not quiet. Gary is young. Harry is not big. Harry is not cold. All young things are cold. If something is rough then it is young. If Erin is big then Erin is young. If Charlie is kind then Charlie is quiet. If something is quiet then it is rough. Kind things are big. Nice things are quiet. If something is cold and rough then it is kind.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Gary is young.
("Gary" "is" "young" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is not cold.
("Harry" "is" "cold" "-")
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is rough then it is young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If Erin is big then Erin is young.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "young" "+"))
If Charlie is kind then Charlie is quiet.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "quiet" "+"))
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If something is cold and rough then it is kind.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Charlie is quiet.
True
1
proof
[(triple1)]
("Charlie" "is" "quiet" "+")
triple1
Harry is cold.
False
1
inv-proof
[(triple7)]
("Harry" "is" "cold" "+")
triple7
Erin is young.
True
2
proof
[(((triple3) -> rule2) OR ((((((triple2 triple3) -> rule8)) -> rule6)) -> rule3))]
("Erin" "is" "young" "+")
((triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((((triple2 triple3) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not kind.
False
3
inv-proof
[(((triple2 triple3) -> rule8) OR ((((((triple3) -> rule2)) -> rule1) triple3) -> rule8))]
("Erin" "is" "kind" "-")
((triple2 triple3) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2)) triple3) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Charlie is young.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("Charlie" "is" "young" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule2))]
("Charlie" "is" "young" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is cold.
True
4
proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule1))]
("Charlie" "is" "cold" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not cold.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule1))]
("Charlie" "is" "cold" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is kind.
True
7
proof
[(((((((((triple1) -> rule5)) -> rule2)) -> rule1) ((triple1) -> rule5)) -> rule8))]
("Charlie" "is" "kind" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule5 % int4))) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is not kind.
False
7
inv-proof
[(((((((((triple1) -> rule5)) -> rule2)) -> rule1) ((triple1) -> rule5)) -> rule8))]
("Charlie" "is" "kind" "-")
((((((((triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule5 % int4))) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is big.
True
8
proof
[(((((((((((triple1) -> rule5)) -> rule2)) -> rule1) ((triple1) -> rule5)) -> rule8)) -> rule6))]
("Charlie" "is" "big" "+")
((((((((((triple1) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule1 % int3)) ((triple1) -> (rule5 % int5))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
int5
Charlie is not big.
False
8
inv-proof
[(((((((((((triple1) -> rule5)) -> rule2)) -> rule1) ((triple1) -> rule5)) -> rule8)) -> rule6))]
("Charlie" "is" "big" "-")
((((((((((triple1) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule1 % int3)) ((triple1) -> (rule5 % int5))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
int5
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is rough.
Unknown
rconc
[@2: Harry is rough.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("Harry" "is" "rough" "+")
Harry is not young.
Unknown
inv-rconc
[@3: Harry is young.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule7 <- FAIL)]]
("Harry" "is" "young" "-")
Gary is big.
Unknown
rconc
[@3: Gary is big.[CWA. Example of deepest failure = (rule6 <- rule8 <- rule5 <- FAIL)]]
("Gary" "is" "big" "+")
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "kind" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "quiet" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is quiet.[(triple1)] Erin is cold.[(triple2 OR ((((triple3) -> rule2)) -> rule1))] Erin is rough.[(triple3)] Gary is not quiet.[(triple4)] Gary is young.[(triple5)] Harry is not big.[(triple6)] Harry is not cold.[(triple7)] @1: Charlie is rough.[(((triple1) -> rule5))] Erin is kind.[(((triple2 triple3) -> rule8) OR ((((((triple3) -> rule2)) -> rule1) triple3) -> rule8))] Erin is young.[(((triple3) -> rule2) OR ((((((triple2 triple3) -> rule8)) -> rule6)) -> rule3))] Gary is cold.[(((triple5) -> rule1))] @2: Charlie is young.[(((((triple1) -> rule5)) -> rule2))] Erin is big.[(((((triple2 triple3) -> rule8)) -> rule6) OR ((((((((triple3) -> rule2)) -> rule1) triple3) -> rule8)) -> rule6))] @3: Charlie is cold.[(((((((triple1) -> rule5)) -> rule2)) -> rule1))] @4: Charlie is kind.[(((((((((triple1) -> rule5)) -> rule2)) -> rule1) ((triple1) -> rule5)) -> rule8))] @5: Charlie is big.[(((((((((((triple1) -> rule5)) -> rule2)) -> rule1) ((triple1) -> rule5)) -> rule8)) -> rule6))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple4
Gary is young.
("Gary" "is" "young" "+")
triple5
Harry is not big.
("Harry" "is" "big" "-")
triple6
Harry is not cold.
("Harry" "is" "cold" "-")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple2 triple3) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2)) triple3) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
((triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((((triple2 triple3) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
((triple5) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((triple2 triple3) -> (rule8 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((((((triple3) -> (rule2 % int4))) -> (rule1 % int3)) triple3) -> (rule8 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule5 % int4))) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is big.
("Charlie" "is" "big" "+")
((((((((((triple1) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule1 % int3)) ((triple1) -> (rule5 % int5))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
int5