Bob is big. Bob is green. Erin is kind. Erin is rough. Gary is nice. Harry is not nice. Harry is round. Kind people are nice. All green people are kind. If Harry is cold then Harry is round.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is round.
("Harry" "is" "round" "+")
Kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
All green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If Harry is cold then Harry is round.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "round" "+"))
Erin is rough.
True
1
proof
[(triple4)]
("Erin" "is" "rough" "+")
triple4
Gary is not nice.
False
1
inv-proof
[(triple5)]
("Gary" "is" "nice" "-")
triple5
Erin is nice.
True
2
proof
[(((triple3) -> rule1))]
("Erin" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("Erin" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Bob is nice.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "nice" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "kind" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "kind" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Bob is big.[(triple1)] Bob is green.[(triple2)] Erin is kind.[(triple3)] Erin is rough.[(triple4)] Gary is nice.[(triple5)] Harry is not nice.[(triple6)] Harry is round.[(triple7)] @1: Bob is kind.[(((triple2) -> rule2))] Erin is nice.[(((triple3) -> rule1))] @2: Bob is nice.[(((((triple2) -> rule2)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Harry is not nice.
("Harry" "is" "nice" "-")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2