Anne is not quiet. Bob is red. Fiona is nice. Gary is nice. Nice things are smart. If something is smart and nice then it is quiet. If something is smart and not nice then it is quiet. Kind things are quiet. If something is quiet then it is blue. If something is blue and not smart then it is round.
Anne is not quiet.
("Anne" "is" "quiet" "-")
Bob is red.
("Bob" "is" "red" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If something is smart and nice then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If something is smart and not nice then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "nice" "~")) -> ("something" "is" "quiet" "+"))
Kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is blue and not smart then it is round.
((("something" "is" "blue" "+") ("something" "is" "smart" "~")) -> ("something" "is" "round" "+"))
Bob is red.
True
1
proof
[(triple2)]
("Bob" "is" "red" "+")
triple2
Bob is not red.
False
1
inv-proof
[(triple2)]
("Bob" "is" "red" "-")
triple2
Gary is smart.
True
2
proof
[(((triple4) -> rule1))]
("Gary" "is" "smart" "+")
((triple4) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple3) -> rule1))]
("Fiona" "is" "smart" "-")
((triple3) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Gary is quiet.
True
4
proof
[(((((triple4) -> rule1) triple4) -> rule2))]
("Gary" "is" "quiet" "+")
((((triple4) -> (rule1 % int2)) triple4) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Fiona is not quiet.
False
4
inv-proof
[(((((triple3) -> rule1) triple3) -> rule2))]
("Fiona" "is" "quiet" "-")
((((triple3) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Anne is blue.
Unknown
rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "blue" "+")
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is not quiet.[(triple1)] Bob is red.[(triple2)] Fiona is nice.[(triple3)] Gary is nice.[(triple4)] @1: Fiona is smart.[(((triple3) -> rule1))] Gary is smart.[(((triple4) -> rule1))] @2: Fiona is quiet.[(((((triple3) -> rule1) triple3) -> rule2))] Gary is quiet.[(((((triple4) -> rule1) triple4) -> rule2))] @3: Fiona is blue.[(((((((triple3) -> rule1) triple3) -> rule2)) -> rule5))] Gary is blue.[(((((((triple4) -> rule1) triple4) -> rule2)) -> rule5))]
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple4) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple4) -> (rule1 % int2)) triple4) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple4) -> (rule1 % int3)) triple4) -> (rule2 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3