Bob is blue. Bob is not furry. Bob is nice. Bob is quiet. Bob is red. Bob is round. Charlie is not blue. Charlie is not furry. Charlie is quiet. Charlie is red. Dave is blue. Dave is furry. Dave is quiet. Dave is not red. Fiona is round. All red people are round. If someone is quiet and not round then they are furry.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not red.
("Dave" "is" "red" "-")
Fiona is round.
("Fiona" "is" "round" "+")
All red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is quiet and not round then they are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "furry" "+"))
Dave is quiet.
True
1
proof
[(triple13)]
("Dave" "is" "quiet" "+")
triple13
Fiona is not round.
False
1
inv-proof
[(triple15)]
("Fiona" "is" "round" "-")
triple15
Charlie is round.
True
2
proof
[(((triple10) -> rule1))]
("Charlie" "is" "round" "+")
((triple10) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple10) -> rule1))]
("Charlie" "is" "round" "-")
((triple10) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "round" "-")
Fiona is furry.
Unknown
rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "furry" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Bob is blue.[(triple1)] Bob is nice.[(triple3)] Bob is not furry.[(triple2)] Bob is quiet.[(triple4)] Bob is red.[(triple5)] Bob is round.[(triple6 OR ((triple5) -> rule1))] Charlie is not blue.[(triple7)] Charlie is not furry.[(triple8)] Charlie is quiet.[(triple9)] Charlie is red.[(triple10)] Dave is blue.[(triple11)] Dave is furry.[(triple12)] Dave is not red.[(triple14)] Dave is quiet.[(triple13)] Fiona is round.[(triple15)] @1: Charlie is round.[(((triple10) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not furry.
("Bob" "is" "furry" "-")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple5) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple7
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple8
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
Charlie is red.
("Charlie" "is" "red" "+")
triple10
Dave is blue.
("Dave" "is" "blue" "+")
triple11
Dave is furry.
("Dave" "is" "furry" "+")
triple12
Dave is not red.
("Dave" "is" "red" "-")
triple14
Dave is quiet.
("Dave" "is" "quiet" "+")
triple13
Fiona is round.
("Fiona" "is" "round" "+")
triple15
Charlie is round.
("Charlie" "is" "round" "+")
((triple10) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1