Bob is smart. Dave is blue. Erin is not red. Harry is green. All green people are blue. All furry, smart people are not red. If someone is furry and green then they are red. All blue people are not red. All smart people are not red. If someone is red then they are round. If someone is red and round then they are not furry. If Harry is red and Harry is smart then Harry is not green.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Erin is not red.
("Erin" "is" "red" "-")
Harry is green.
("Harry" "is" "green" "+")
All green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
All furry, smart people are not red.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "-"))
If someone is furry and green then they are red.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
All blue people are not red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "-"))
All smart people are not red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "-"))
If someone is red then they are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is red and round then they are not furry.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "-"))
If Harry is red and Harry is smart then Harry is not green.
((("Harry" "is" "red" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "green" "-"))
Harry is green.
True
1
proof
[(triple4)]
("Harry" "is" "green" "+")
triple4
Erin is red.
False
1
inv-proof
[(triple3)]
("Erin" "is" "red" "+")
triple3
Dave is not red.
True
2
proof
[(((triple2) -> rule4))]
("Dave" "is" "red" "-")
((triple2) -> (rule4 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is red.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "red" "+")
((triple2) -> (rule4 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Harry is not red.
True
3
proof
[(((((triple4) -> rule1)) -> rule4))]
("Harry" "is" "red" "-")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is red.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule4))]
("Harry" "is" "red" "+")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "round" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "blue" "+")
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Bob is smart.[(triple1)] Dave is blue.[(triple2)] Erin is not red.[(triple3)] Harry is green.[(triple4)] @1: Bob is not red.[(((triple1) -> rule5))] Dave is not red.[(((triple2) -> rule4))] Harry is blue.[(((triple4) -> rule1))] @2: Harry is not red.[(((((triple4) -> rule1)) -> rule4))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Erin is not red.
("Erin" "is" "red" "-")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Bob is not red.
("Bob" "is" "red" "-")
((triple1) -> (rule5 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Dave is not red.
("Dave" "is" "red" "-")
((triple2) -> (rule4 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not red.
("Harry" "is" "red" "-")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2