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