Bob is nice. Charlie is round. Erin is kind. Harry is green. Nice things are green. If something is cold and kind then it is round. If something is green then it is quiet.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Harry is green.
("Harry" "is" "green" "+")
Nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is cold and kind then it is round.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If something is green then it is quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Erin is kind.
True
1
proof
[(triple3)]
("Erin" "is" "kind" "+")
triple3
Erin is not kind.
False
1
inv-proof
[(triple3)]
("Erin" "is" "kind" "-")
triple3
Harry is quiet.
True
2
proof
[(((triple4) -> rule3))]
("Harry" "is" "quiet" "+")
((triple4) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "green" "-")
((triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not quiet.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Bob" "is" "quiet" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "green" "-")
Bob is round.
Unknown
rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "round" "+")
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "round" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Bob is nice.[(triple1)] Charlie is round.[(triple2)] Erin is kind.[(triple3)] Harry is green.[(triple4)] @1: Bob is green.[(((triple1) -> rule1))] Harry is quiet.[(((triple4) -> rule3))] @2: Bob is quiet.[(((((triple1) -> rule1)) -> rule3))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2