Dave is cold. Dave is kind. Dave is round. Dave is not white. Fiona is not cold. Fiona is quiet. Fiona is rough. Fiona is smart. Fiona is white. Harry is cold. Harry is kind. Harry is quiet. Harry is rough. Harry is round. Harry is white. If Harry is white and Harry is not rough then Harry is smart. If someone is cold then they are smart. Smart people are quiet. If someone is quiet and not smart then they are not kind. All kind people are round. If Fiona is rough and Fiona is round then Fiona is not quiet.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is not white.
("Dave" "is" "white" "-")
Fiona is not cold.
("Fiona" "is" "cold" "-")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If Harry is white and Harry is not rough then Harry is smart.
((("Harry" "is" "white" "+") ("Harry" "is" "rough" "~")) -> ("Harry" "is" "smart" "+"))
If someone is cold then they are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet and not smart then they are not kind.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "kind" "-"))
All kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If Fiona is rough and Fiona is round then Fiona is not quiet.
((("Fiona" "is" "rough" "+") ("Fiona" "is" "round" "+")) -> ("Fiona" "is" "quiet" "-"))
Dave is round.
True
1
proof
[(triple3 OR ((triple2) -> rule5))]
("Dave" "is" "round" "+")
triple3
((triple2) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Fiona is not rough.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "rough" "-")
triple7
Dave is smart.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Dave" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not quiet.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Dave" "is" "quiet" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "round" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Dave is cold.[(triple1)] Dave is kind.[(triple2)] Dave is not white.[(triple4)] Dave is round.[(triple3 OR ((triple2) -> rule5))] Fiona is not cold.[(triple5)] Fiona is quiet.[(triple6 OR ((triple8) -> rule3))] Fiona is rough.[(triple7)] Fiona is smart.[(triple8)] Fiona is white.[(triple9)] Harry is cold.[(triple10)] Harry is kind.[(triple11)] Harry is quiet.[(triple12 OR ((((triple10) -> rule2)) -> rule3))] Harry is rough.[(triple13)] Harry is round.[(triple14 OR ((triple11) -> rule5))] Harry is white.[(triple15)] @1: Dave is smart.[(((triple1) -> rule2))] Harry is smart.[(((triple10) -> rule2))] @2: Dave is quiet.[(((((triple1) -> rule2)) -> rule3))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is not white.
("Dave" "is" "white" "-")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple3
((triple2) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple5
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
((triple8) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple7
Fiona is smart.
("Fiona" "is" "smart" "+")
triple8
Fiona is white.
("Fiona" "is" "white" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
((triple11) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple15
Dave is smart.
("Dave" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple10) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2