Bob is cold. Bob is red. Bob is smart. Bob is white. Erin is cold. Erin is red. Erin is smart. Erin is white. Harry is green. Harry is not young. Green things are smart. If something is round and green then it is smart. Round things are not white. If something is young and not cold then it is white. If something is round and white then it is green. If Harry is young then Harry is white. If Harry is green and Harry is round then Harry is not white. Green things are round.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is not young.
("Harry" "is" "young" "-")
Green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is round and green then it is smart.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Round things are not white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "-"))
If something is young and not cold then it is white.
((("something" "is" "young" "+") ("something" "is" "cold" "~")) -> ("something" "is" "white" "+"))
If something is round and white then it is green.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If Harry is young then Harry is white.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "white" "+"))
If Harry is green and Harry is round then Harry is not white.
((("Harry" "is" "green" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "white" "-"))
Green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Bob is smart.
True
1
proof
[(triple3)]
("Bob" "is" "smart" "+")
triple3
Bob is not white.
False
1
inv-proof
[(triple4)]
("Bob" "is" "white" "-")
triple4
Harry is smart.
True
2
proof
[(((triple9) -> rule1) OR ((((triple9) -> rule8) triple9) -> rule2))]
("Harry" "is" "smart" "+")
((triple9) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple9) -> (rule8 % int2)) triple9) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not smart.
False
2
inv-proof
[(((triple9) -> rule1) OR ((((triple9) -> rule8) triple9) -> rule2))]
("Harry" "is" "smart" "-")
((triple9) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple9) -> (rule8 % int2)) triple9) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not white.
True
3
proof
[(((((triple9) -> rule8)) -> rule3) OR ((triple9 ((triple9) -> rule8)) -> rule7))]
("Harry" "is" "white" "-")
((((triple9) -> (rule8 % int2))) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple9 ((triple9) -> (rule8 % int2))) -> (rule7 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
False
3
inv-proof
[(((((triple9) -> rule8)) -> rule3) OR ((triple9 ((triple9) -> rule8)) -> rule7))]
("Harry" "is" "white" "+")
((((triple9) -> (rule8 % int2))) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple9 ((triple9) -> (rule8 % int2))) -> (rule7 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Erin is not round.
Unknown
inv-rconc
[@2: Erin is round.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("Erin" "is" "round" "-")
Bob is green.
Unknown
rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("Bob" "is" "green" "+")
Erin is not green.
Unknown
inv-rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("Erin" "is" "green" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Bob is cold.[(triple1)] Bob is red.[(triple2)] Bob is smart.[(triple3)] Bob is white.[(triple4)] Erin is cold.[(triple5)] Erin is red.[(triple6)] Erin is smart.[(triple7)] Erin is white.[(triple8)] Harry is green.[(triple9)] Harry is not young.[(triple10)] @1: Harry is round.[(((triple9) -> rule8))] Harry is smart.[(((triple9) -> rule1) OR ((((triple9) -> rule8) triple9) -> rule2))] @2: Harry is not white.[(((((triple9) -> rule8)) -> rule3) OR ((triple9 ((triple9) -> rule8)) -> rule7))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is not young.
("Harry" "is" "young" "-")
triple10
Harry is round.
("Harry" "is" "round" "+")
((triple9) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple9) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple9) -> (rule8 % int2)) triple9) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not white.
("Harry" "is" "white" "-")
((((triple9) -> (rule8 % int2))) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple9 ((triple9) -> (rule8 % int2))) -> (rule7 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2