Bob is blue. Dave is nice. Fiona is round. If someone is blue then they are smart. If Fiona is round then Fiona is big. If Bob is blue and Bob is smart then Bob is not quiet.
Bob is blue.
("Bob" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If someone is blue then they are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If Fiona is round then Fiona is big.
((("Fiona" "is" "round" "+")) -> ("Fiona" "is" "big" "+"))
If Bob is blue and Bob is smart then Bob is not quiet.
((("Bob" "is" "blue" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "quiet" "-"))
Dave is nice.
True
1
proof
[(triple2)]
("Dave" "is" "nice" "+")
triple2
Fiona is not round.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "round" "-")
triple3
Bob is smart.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "smart" "-")
((triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not quiet.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule3))]
("Bob" "is" "quiet" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule3))]
("Bob" "is" "quiet" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "smart" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "smart" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Bob is blue.[(triple1)] Dave is nice.[(triple2)] Fiona is round.[(triple3)] @1: Bob is smart.[(((triple1) -> rule1))] Fiona is big.[(((triple3) -> rule2))] @2: Bob is not quiet.[(((triple1 ((triple1) -> rule1)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple3) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Bob is not quiet.
("Bob" "is" "quiet" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2