Charlie is rough. Fiona is round. Fiona is white. Gary is red. Gary is rough. Gary is round. Harry is rough. If Charlie is red and Charlie is nice then Charlie is round. If Gary is nice then Gary is rough. If someone is nice and rough then they are white. Round people are nice. If someone is quiet then they are nice. If someone is round and nice then they are cold. All rough people are quiet. All round people are cold.
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Charlie is red and Charlie is nice then Charlie is round.
((("Charlie" "is" "red" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "round" "+"))
If Gary is nice then Gary is rough.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "rough" "+"))
If someone is nice and rough then they are white.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone is quiet then they are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If someone is round and nice then they are cold.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
All rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
All round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Harry is rough.
True
1
proof
[(triple7)]
("Harry" "is" "rough" "+")
triple7
Charlie is not rough.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "rough" "-")
triple1
Harry is quiet.
True
2
proof
[(((triple7) -> rule7))]
("Harry" "is" "quiet" "+")
((triple7) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple5) -> rule7) OR ((((((triple6) -> rule4)) -> rule2)) -> rule7))]
("Gary" "is" "quiet" "-")
((triple5) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Charlie is cold.
Unknown
rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "cold" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Charlie is rough.[(triple1)] Fiona is round.[(triple2)] Fiona is white.[(triple3)] Gary is red.[(triple4)] Gary is rough.[(triple5 OR ((((triple6) -> rule4)) -> rule2))] Gary is round.[(triple6)] Harry is rough.[(triple7)] @1: Charlie is quiet.[(((triple1) -> rule7))] Fiona is cold.[(((triple2) -> rule8) OR ((triple2 ((triple2) -> rule4)) -> rule6))] Fiona is nice.[(((triple2) -> rule4))] Gary is cold.[(((triple6) -> rule8) OR ((triple6 ((triple6) -> rule4)) -> rule6) OR ((triple6 ((((triple5) -> rule7)) -> rule5)) -> rule6))] Gary is nice.[(((triple6) -> rule4) OR ((((triple5) -> rule7)) -> rule5))] Gary is quiet.[(((triple5) -> rule7) OR ((((((triple6) -> rule4)) -> rule2)) -> rule7))] Harry is quiet.[(((triple7) -> rule7))] @2: Charlie is nice.[(((((triple1) -> rule7)) -> rule5))] Gary is white.[(((((triple6) -> rule4) triple5) -> rule3) OR ((((((triple5) -> rule7)) -> rule5) triple5) -> rule3) OR ((((triple6) -> rule4) ((((triple6) -> rule4)) -> rule2)) -> rule3) OR ((((((triple5) -> rule7)) -> rule5) ((((triple6) -> rule4)) -> rule2)) -> rule3))] Harry is nice.[(((((triple7) -> rule7)) -> rule5))] @3: Charlie is white.[(((((((triple1) -> rule7)) -> rule5) triple1) -> rule3))] Harry is white.[(((((((triple7) -> rule7)) -> rule5) triple7) -> rule3))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Fiona is round.
("Fiona" "is" "round" "+")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple5
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple2) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple2 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple6) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple6 ((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((triple6 ((((triple5) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
((triple6) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple5) -> (rule7 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple5) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple7) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple6) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((((triple5) -> (rule7 % int3))) -> (rule5 % int2)) triple5) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((triple6) -> (rule4 % int3)) ((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple5) -> (rule7 % int4))) -> (rule5 % int3)) ((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
((((triple7) -> (rule7 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2)) triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((((((triple7) -> (rule7 % int3))) -> (rule5 % int2)) triple7) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3