Charlie is cold. Fiona is not rough. Fiona is round. Gary is cold. Gary is quiet. Gary is round. Gary is smart. Harry is not cold. Harry is quiet. Harry is smart. If something is nice then it is smart. All rough things are smart. All cold things are rough. If Harry is quiet and Harry is white then Harry is not round. Smart, round things are not white. Cold, smart things are quiet. If Fiona is not rough then Fiona is not smart. Quiet, white things are not round.
Charlie is cold.
("Charlie" "is" "cold" "+")
Fiona is not rough.
("Fiona" "is" "rough" "-")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
All rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
All cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If Harry is quiet and Harry is white then Harry is not round.
((("Harry" "is" "quiet" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "round" "-"))
Smart, round things are not white.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "-"))
Cold, smart things are quiet.
((("something" "is" "cold" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If Fiona is not rough then Fiona is not smart.
((("Fiona" "is" "rough" "~")) -> ("Fiona" "is" "smart" "-"))
Quiet, white things are not round.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "round" "-"))
Fiona is round.
True
1
proof
[(triple3)]
("Fiona" "is" "round" "+")
triple3
Gary is not round.
False
1
inv-proof
[(triple6)]
("Gary" "is" "round" "-")
triple6
Gary is not white.
True
3
proof
[(((triple7 triple6) -> rule5) OR ((((((triple4) -> rule3)) -> rule2) triple6) -> rule5))]
("Gary" "is" "white" "-")
((triple7 triple6) -> (rule5 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2)) triple6) -> (rule5 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Fiona is smart.
False
2
inv-proof
[(((triple2) -> rule7))]
("Fiona" "is" "smart" "+")
((triple2) -> (rule7 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "rough" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Charlie is cold.[(triple1)] Fiona is not rough.[(triple2)] Fiona is round.[(triple3)] Gary is cold.[(triple4)] Gary is quiet.[(triple5 OR ((triple4 triple7) -> rule6) OR ((triple4 ((((triple4) -> rule3)) -> rule2)) -> rule6))] Gary is round.[(triple6)] Gary is smart.[(triple7 OR ((((triple4) -> rule3)) -> rule2))] Harry is not cold.[(triple8)] Harry is quiet.[(triple9)] Harry is smart.[(triple10)] @1: Charlie is rough.[(((triple1) -> rule3))] Fiona is not smart.[(((triple2) -> rule7))] Gary is not white.[(((triple7 triple6) -> rule5) OR ((((((triple4) -> rule3)) -> rule2) triple6) -> rule5))] Gary is rough.[(((triple4) -> rule3))] @2: Charlie is smart.[(((((triple1) -> rule3)) -> rule2))] @3: Charlie is quiet.[(((triple1 ((((triple1) -> rule3)) -> rule2)) -> rule6))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple2
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
((triple4 triple7) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple4 ((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Harry is not cold.
("Harry" "is" "cold" "-")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Fiona is not smart.
("Fiona" "is" "smart" "-")
((triple2) -> (rule7 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Gary is not white.
("Gary" "is" "white" "-")
((triple7 triple6) -> (rule5 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2)) triple6) -> (rule5 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3