Bob is blue. Bob is cold. Bob is green. Bob is round. Charlie is cold. Charlie is not furry. Charlie is green. Harry is big. Harry is blue. Harry is round. All round things are green. All furry things are round. If something is green then it is not red.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is round.
("Harry" "is" "round" "+")
All round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
All furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If something is green then it is not red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "-"))
Bob is cold.
True
1
proof
[(triple2)]
("Bob" "is" "cold" "+")
triple2
Charlie is not green.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "green" "-")
triple7
Bob is not red.
True
2
proof
[(((triple3) -> rule3) OR ((((triple4) -> rule1)) -> rule3))]
("Bob" "is" "red" "-")
((triple3) -> (rule3 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is red.
False
2
inv-proof
[(((triple3) -> rule3) OR ((((triple4) -> rule1)) -> rule3))]
("Bob" "is" "red" "+")
((triple3) -> (rule3 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "round" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is green.[(triple3 OR ((triple4) -> rule1))] Bob is round.[(triple4)] Charlie is cold.[(triple5)] Charlie is green.[(triple7)] Charlie is not furry.[(triple6)] Harry is big.[(triple8)] Harry is blue.[(triple9)] Harry is round.[(triple10)] @1: Bob is not red.[(((triple3) -> rule3) OR ((((triple4) -> rule1)) -> rule3))] Charlie is not red.[(((triple7) -> rule3))] Harry is green.[(((triple10) -> rule1))] @2: Harry is not red.[(((((triple10) -> rule1)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
((triple4) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
Bob is not red.
("Bob" "is" "red" "-")
((triple3) -> (rule3 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Charlie is not red.
("Charlie" "is" "red" "-")
((triple7) -> (rule3 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple10) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not red.
("Harry" "is" "red" "-")
((((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2