Bob is nice. Bob is quiet. Charlie is furry. Charlie is green. Charlie is kind. Charlie is nice. Charlie is quiet. Erin is furry. Erin is green. Erin is nice. All round, green people are young. If Erin is green then Erin is quiet. Kind, green people are round.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
All round, green people are young.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If Erin is green then Erin is quiet.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "quiet" "+"))
Kind, green people are round.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Bob is quiet.
True
1
proof
[(triple2)]
("Bob" "is" "quiet" "+")
triple2
Charlie is not furry.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "furry" "-")
triple3
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "young" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is nice.[(triple1)] Bob is quiet.[(triple2)] Charlie is furry.[(triple3)] Charlie is green.[(triple4)] Charlie is kind.[(triple5)] Charlie is nice.[(triple6)] Charlie is quiet.[(triple7)] Erin is furry.[(triple8)] Erin is green.[(triple9)] Erin is nice.[(triple10)] @1: Charlie is round.[(((triple5 triple4) -> rule3))] Erin is quiet.[(((triple9) -> rule2))] @2: Charlie is young.[(((((triple5 triple4) -> rule3) triple4) -> rule1))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
Erin is furry.
("Erin" "is" "furry" "+")
triple8
Erin is green.
("Erin" "is" "green" "+")
triple9
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Charlie is round.
("Charlie" "is" "round" "+")
((triple5 triple4) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple9) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple5 triple4) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2