Anne is round. Bob is smart. Fiona is blue. Harry is furry. If Bob is blue and Bob is cold then Bob is furry. If someone is green and cold then they are blue. Smart people are furry. Furry people are blue. Smart people are green. If someone is round and green then they are blue.
Anne is round.
("Anne" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If Bob is blue and Bob is cold then Bob is furry.
((("Bob" "is" "blue" "+") ("Bob" "is" "cold" "+")) -> ("Bob" "is" "furry" "+"))
If someone is green and cold then they are blue.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
Furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
Smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is round and green then they are blue.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Bob is smart.
True
1
proof
[(triple2)]
("Bob" "is" "smart" "+")
triple2
Bob is not smart.
False
1
inv-proof
[(triple2)]
("Bob" "is" "smart" "-")
triple2
Bob is furry.
True
2
proof
[(((triple2) -> rule3))]
("Bob" "is" "furry" "+")
((triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple2) -> rule5))]
("Bob" "is" "green" "-")
((triple2) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "green" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "green" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is round.[(triple1)] Bob is smart.[(triple2)] Fiona is blue.[(triple3)] Harry is furry.[(triple4)] @1: Bob is furry.[(((triple2) -> rule3))] Bob is green.[(((triple2) -> rule5))] Harry is blue.[(((triple4) -> rule4))] @2: Bob is blue.[(((((triple2) -> rule3)) -> rule4))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Bob is furry.
("Bob" "is" "furry" "+")
((triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2