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