Anne is kind. Bob is rough. Fiona is green. Harry is kind. All white, rough things are green. Red, green things are smart. If something is rough then it is white. All green, nice things are red. Rough things are red. If something is green and red then it is nice.
Anne is kind.
("Anne" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All white, rough things are green.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Red, green things are smart.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is rough then it is white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
All green, nice things are red.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
Rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something is green and red then it is nice.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Bob is not rough.
False
1
inv-proof
[(triple2)]
("Bob" "is" "rough" "-")
triple2
Bob is white.
True
2
proof
[(((triple2) -> rule3))]
("Bob" "is" "white" "+")
((triple2) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple2) -> rule5))]
("Bob" "is" "red" "-")
((triple2) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "white" "-")
Fiona is smart.
Unknown
rconc
[@4: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule6 <- rule5 <- FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Bob is rough.[(triple2)] Fiona is green.[(triple3)] Harry is kind.[(triple4)] @1: Bob is red.[(((triple2) -> rule5))] Bob is white.[(((triple2) -> rule3))] @2: Bob is green.[(((((triple2) -> rule3) triple2) -> rule1))] @3: Bob is nice.[(((((((triple2) -> rule3) triple2) -> rule1) ((triple2) -> rule5)) -> rule6))] Bob is smart.[(((((triple2) -> rule5) ((((triple2) -> rule3) triple2) -> rule1)) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple2) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((((((triple2) -> (rule3 % int4)) triple2) -> (rule1 % int3)) ((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
((((triple2) -> (rule5 % int4)) ((((triple2) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4