Bob is quiet. Bob is smart. Dave is cold. Dave is nice. Dave is rough. Fiona is cold. Fiona is green. Fiona is nice. Fiona is quiet. Fiona is rough. Fiona is smart. Fiona is white. Harry is not cold. Harry is quiet. Harry is rough. Harry is white. All smart, nice people are green. If someone is nice then they are smart. If Harry is smart and Harry is white then Harry is green.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
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 not cold.
("Harry" "is" "cold" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
All smart, nice people are green.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is nice then they are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If Harry is smart and Harry is white then Harry is green.
((("Harry" "is" "smart" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "green" "+"))
Fiona is white.
True
1
proof
[(triple12)]
("Fiona" "is" "white" "+")
triple12
Harry is not white.
False
1
inv-proof
[(triple16)]
("Harry" "is" "white" "-")
triple16
Dave is smart.
True
2
proof
[(((triple4) -> rule2))]
("Dave" "is" "smart" "+")
((triple4) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple4) -> rule2))]
("Dave" "is" "smart" "-")
((triple4) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
True
4
proof
[(((((triple4) -> rule2) triple4) -> rule1))]
("Dave" "is" "green" "+")
((((triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not green.
False
4
inv-proof
[(((((triple4) -> rule2) triple4) -> rule1))]
("Dave" "is" "green" "-")
((((triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Harry is not green.
Unknown
inv-rconc
[@2: Harry is green.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Harry" "is" "green" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "smart" "+")
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is quiet.[(triple1)] Bob is smart.[(triple2)] Dave is cold.[(triple3)] Dave is nice.[(triple4)] Dave is rough.[(triple5)] Fiona is cold.[(triple6)] Fiona is green.[(triple7 OR ((triple11 triple8) -> rule1) OR ((((triple8) -> rule2) triple8) -> rule1))] Fiona is nice.[(triple8)] Fiona is quiet.[(triple9)] Fiona is rough.[(triple10)] Fiona is smart.[(triple11 OR ((triple8) -> rule2))] Fiona is white.[(triple12)] Harry is not cold.[(triple13)] Harry is quiet.[(triple14)] Harry is rough.[(triple15)] Harry is white.[(triple16)] @1: Dave is smart.[(((triple4) -> rule2))] @2: Dave is green.[(((((triple4) -> rule2) triple4) -> rule1))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Fiona is green.
("Fiona" "is" "green" "+")
triple7
((triple11 triple8) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple8) -> (rule2 % int2)) triple8) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple8
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Fiona is rough.
("Fiona" "is" "rough" "+")
triple10
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
((triple8) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple12
Harry is not cold.
("Harry" "is" "cold" "-")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
Dave is smart.
("Dave" "is" "smart" "+")
((triple4) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2