Bob is smart. Charlie is smart. Erin is cold. Gary is blue. Cold things are blue. Blue things are quiet. If Gary is not quiet then Gary is green.
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If Gary is not quiet then Gary is green.
((("Gary" "is" "quiet" "~")) -> ("Gary" "is" "green" "+"))
Bob is smart.
True
1
proof
[(triple1)]
("Bob" "is" "smart" "+")
triple1
Bob is not smart.
False
1
inv-proof
[(triple1)]
("Bob" "is" "smart" "-")
triple1
Gary is quiet.
True
2
proof
[(((triple4) -> rule2))]
("Gary" "is" "quiet" "+")
((triple4) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple4) -> rule2))]
("Gary" "is" "quiet" "-")
((triple4) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Erin is quiet.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("Erin" "is" "quiet" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not quiet.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("Erin" "is" "quiet" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Charlie is not quiet.
Unknown
inv-rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is smart.[(triple1)] Charlie is smart.[(triple2)] Erin is cold.[(triple3)] Gary is blue.[(triple4)] @1: Erin is blue.[(((triple3) -> rule1))] Gary is quiet.[(((triple4) -> rule2))] @2: Erin is quiet.[(((((triple3) -> rule1)) -> rule2))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple4) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2