Bob is green. Bob is nice. Bob is young. Dave is smart. Dave is white. Fiona is green. Fiona is not red. Fiona is smart. Fiona is white. Fiona is not young. If Bob is red then Bob is not smart. If something is nice then it is red. If something is quiet then it is green.
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is not red.
("Fiona" "is" "red" "-")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
If Bob is red then Bob is not smart.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "smart" "-"))
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Fiona is red.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "red" "+")
triple7
Bob is red.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "red" "+")
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "red" "-")
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not smart.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "smart" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is smart.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "red" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "green" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Bob is green.[(triple1)] Bob is nice.[(triple2)] Bob is young.[(triple3)] Dave is smart.[(triple4)] Dave is white.[(triple5)] Fiona is green.[(triple6)] Fiona is not red.[(triple7)] Fiona is not young.[(triple10)] Fiona is smart.[(triple8)] Fiona is white.[(triple9)] @1: Bob is red.[(((triple2) -> rule2))] @2: Bob is not smart.[(((((triple2) -> rule2)) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Fiona is not red.
("Fiona" "is" "red" "-")
triple7
Fiona is not young.
("Fiona" "is" "young" "-")
triple10
Fiona is smart.
("Fiona" "is" "smart" "+")
triple8
Fiona is white.
("Fiona" "is" "white" "+")
triple9
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not smart.
("Bob" "is" "smart" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2