Anne is smart. Bob is white. Fiona is red. Harry is furry. Furry people are white. All white people are not green. If Bob is round then Bob is not kind.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
All white people are not green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "-"))
If Bob is round then Bob is not kind.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "kind" "-"))
Anne is smart.
True
1
proof
[(triple1)]
("Anne" "is" "smart" "+")
triple1
Fiona is not red.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "red" "-")
triple3
Harry is white.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "white" "+")
((triple4) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple4) -> rule1))]
("Harry" "is" "white" "-")
((triple4) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not green.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("Harry" "is" "green" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("Harry" "is" "green" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "white" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "white" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Anne is smart.[(triple1)] Bob is white.[(triple2)] Fiona is red.[(triple3)] Harry is furry.[(triple4)] @1: Bob is not green.[(((triple2) -> rule2))] Harry is white.[(((triple4) -> rule1))] @2: Harry is not green.[(((((triple4) -> rule1)) -> rule2))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Bob is not green.
("Bob" "is" "green" "-")
((triple2) -> (rule2 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not green.
("Harry" "is" "green" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2