Bob is not green. Bob is kind. Fiona is round. Fiona is smart. Harry is furry. Harry is kind. Harry is not quiet. Smart people are furry. If Bob is kind then Bob is round. If Bob is green and Bob is white then Bob is not round. If someone is white then they are round. If Fiona is furry and Fiona is green then Fiona is not round. All round people are smart.
Bob is not green.
("Bob" "is" "green" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If Bob is kind then Bob is round.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "round" "+"))
If Bob is green and Bob is white then Bob is not round.
((("Bob" "is" "green" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "round" "-"))
If someone is white then they are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If Fiona is furry and Fiona is green then Fiona is not round.
((("Fiona" "is" "furry" "+") ("Fiona" "is" "green" "+")) -> ("Fiona" "is" "round" "-"))
All round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Fiona is round.
True
1
proof
[(triple3)]
("Fiona" "is" "round" "+")
triple3
Bob is not kind.
False
1
inv-proof
[(triple2)]
("Bob" "is" "kind" "-")
triple2
Bob is round.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "round" "+")
((triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "round" "-")
((triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
True
3
proof
[(((((triple2) -> rule2)) -> rule6))]
("Bob" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule6))]
("Bob" "is" "smart" "-")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is furry.
True
4
proof
[(((((((triple2) -> rule2)) -> rule6)) -> rule1))]
("Bob" "is" "furry" "+")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not furry.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule6)) -> rule1))]
("Bob" "is" "furry" "-")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Harry is not smart.
Unknown
inv-rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "round" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Bob is kind.[(triple2)] Bob is not green.[(triple1)] Fiona is round.[(triple3)] Fiona is smart.[(triple4 OR ((triple3) -> rule6))] Harry is furry.[(triple5)] Harry is kind.[(triple6)] Harry is not quiet.[(triple7)] @1: Bob is round.[(((triple2) -> rule2))] Fiona is furry.[(((triple4) -> rule1) OR ((((triple3) -> rule6)) -> rule1))] @2: Bob is smart.[(((((triple2) -> rule2)) -> rule6))] @3: Bob is furry.[(((((((triple2) -> rule2)) -> rule6)) -> rule1))]
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is not green.
("Bob" "is" "green" "-")
triple1
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple4
((triple3) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple7
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3