Bob is nice. Erin is round. Gary is young. Harry is young. Kind things are green. If something is kind then it is rough. If something is furry then it is rough. Round things are kind. All round things are nice. Young things are round.
Bob is nice.
("Bob" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is young.
("Harry" "is" "young" "+")
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is furry then it is rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
Round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
All round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
Gary is young.
True
1
proof
[(triple3)]
("Gary" "is" "young" "+")
triple3
Gary is not young.
False
1
inv-proof
[(triple3)]
("Gary" "is" "young" "-")
triple3
Harry is round.
True
2
proof
[(((triple4) -> rule6))]
("Harry" "is" "round" "+")
((triple4) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple4) -> rule6))]
("Harry" "is" "round" "-")
((triple4) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
True
3
proof
[(((((triple4) -> rule6)) -> rule4))]
("Harry" "is" "kind" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule5))]
("Harry" "is" "nice" "-")
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Gary is green.
True
4
proof
[(((((((triple3) -> rule6)) -> rule4)) -> rule1))]
("Gary" "is" "green" "+")
((((((triple3) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is not green.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule4)) -> rule1))]
("Gary" "is" "green" "-")
((((((triple3) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is rough.
Unknown
rconc
[@3: Bob is rough.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule6 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not kind.
Unknown
inv-rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is green.
Unknown
rconc
[@3: Bob is green.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule6 <- FAIL)]]
("Bob" "is" "green" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Bob is nice.[(triple1)] Erin is round.[(triple2)] Gary is young.[(triple3)] Harry is young.[(triple4)] @1: Erin is kind.[(((triple2) -> rule4))] Erin is nice.[(((triple2) -> rule5))] Gary is round.[(((triple3) -> rule6))] Harry is round.[(((triple4) -> rule6))] @2: Erin is green.[(((((triple2) -> rule4)) -> rule1))] Erin is rough.[(((((triple2) -> rule4)) -> rule2))] Gary is kind.[(((((triple3) -> rule6)) -> rule4))] Gary is nice.[(((((triple3) -> rule6)) -> rule5))] Harry is kind.[(((((triple4) -> rule6)) -> rule4))] Harry is nice.[(((((triple4) -> rule6)) -> rule5))] @3: Gary is green.[(((((((triple3) -> rule6)) -> rule4)) -> rule1))] Gary is rough.[(((((((triple3) -> rule6)) -> rule4)) -> rule2))] Harry is green.[(((((((triple4) -> rule6)) -> rule4)) -> rule1))] Harry is rough.[(((((((triple4) -> rule6)) -> rule4)) -> rule2))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Erin is round.
("Erin" "is" "round" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple3) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple4) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((((triple3) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((((((triple3) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3