Bob is rough. Fiona is green. If something is rough then it is green. If something is green then it is quiet. All green things are nice. If something is blue and nice then it is green. Smart, nice things are young. If Fiona is rough then Fiona is quiet.
Bob is rough.
("Bob" "is" "rough" "+")
Fiona is green.
("Fiona" "is" "green" "+")
If something is rough then it is green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is green then it is quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is blue and nice then it is green.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Smart, nice things are young.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If Fiona is rough then Fiona is quiet.
((("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "quiet" "+"))
Bob is rough.
True
1
proof
[(triple1)]
("Bob" "is" "rough" "+")
triple1
Bob is not rough.
False
1
inv-proof
[(triple1)]
("Bob" "is" "rough" "-")
triple1
Fiona is nice.
True
2
proof
[(((triple2) -> rule3))]
("Fiona" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not quiet.
False
2
inv-proof
[(((triple2) -> rule2))]
("Fiona" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Bob is nice.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not quiet.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "quiet" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "young" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Bob is rough.[(triple1)] Fiona is green.[(triple2)] @1: Bob is green.[(((triple1) -> rule1))] Fiona is nice.[(((triple2) -> rule3))] Fiona is quiet.[(((triple2) -> rule2))] @2: Bob is nice.[(((((triple1) -> rule1)) -> rule3))] Bob is quiet.[(((((triple1) -> rule1)) -> rule2))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Fiona is green.
("Fiona" "is" "green" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2