Bob is furry. Bob is quiet. Bob is rough. Bob is white. Charlie is big. Charlie is rough. Erin is quiet. Erin is red. Harry is big. Harry is furry. If something is big and furry then it is white. All white, furry things are red. All furry, white things are big.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If something is big and furry then it is white.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
All white, furry things are red.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
All furry, white things are big.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Bob is white.
True
1
proof
[(triple4)]
("Bob" "is" "white" "+")
triple4
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Bob is big.
True
3
proof
[(((triple1 triple4) -> rule3))]
("Bob" "is" "big" "+")
((triple1 triple4) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not big.
False
3
inv-proof
[(((triple1 triple4) -> rule3))]
("Bob" "is" "big" "-")
((triple1 triple4) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Harry is red.
True
5
proof
[(((((triple9 triple10) -> rule1) triple10) -> rule2))]
("Harry" "is" "red" "+")
((((triple9 triple10) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not red.
False
5
inv-proof
[(((((triple9 triple10) -> rule1) triple10) -> rule2))]
("Harry" "is" "red" "-")
((((triple9 triple10) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "white" "+")
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "big" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Bob is furry.[(triple1)] Bob is quiet.[(triple2)] Bob is rough.[(triple3)] Bob is white.[(triple4)] Charlie is big.[(triple5)] Charlie is rough.[(triple6)] Erin is quiet.[(triple7)] Erin is red.[(triple8)] Harry is big.[(triple9)] Harry is furry.[(triple10)] @1: Bob is big.[(((triple1 triple4) -> rule3))] Bob is red.[(((triple4 triple1) -> rule2))] Harry is white.[(((triple9 triple10) -> rule1))] @2: Harry is red.[(((((triple9 triple10) -> rule1) triple10) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple8
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Bob is big.
("Bob" "is" "big" "+")
((triple1 triple4) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple4 triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple9 triple10) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((((triple9 triple10) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2