Bob is rough. Bob is round. Bob is young. Fiona is not cold. Fiona is quiet. Gary is blue. Gary is rough. If Gary is young then Gary is blue. If something is round then it is blue. All round, blue things are young. All rough, young things are not kind. All blue things are round. All blue things are rough.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Fiona is not cold.
("Fiona" "is" "cold" "-")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Gary is young then Gary is blue.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "blue" "+"))
If something is round then it is blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
All round, blue things are young.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All rough, young things are not kind.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "-"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Gary is rough.
True
1
proof
[(triple7 OR ((triple6) -> rule6))]
("Gary" "is" "rough" "+")
triple7
((triple6) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Bob is not young.
False
1
inv-proof
[(triple3 OR ((triple2 ((triple2) -> rule2)) -> rule3))]
("Bob" "is" "young" "-")
triple3
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not kind.
True
3
proof
[(((triple1 triple3) -> rule4) OR ((triple1 ((triple2 ((triple2) -> rule2)) -> rule3)) -> rule4) OR ((((((triple2) -> rule2)) -> rule6) triple3) -> rule4) OR ((((((triple2) -> rule2)) -> rule6) ((triple2 ((triple2) -> rule2)) -> rule3)) -> rule4))]
("Bob" "is" "kind" "-")
((triple1 triple3) -> (rule4 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
((triple1 ((triple2 ((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2)) triple3) -> (rule4 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((triple2) -> (rule2 % int4))) -> (rule6 % int3)) ((triple2 ((triple2) -> (rule2 % int4))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is not blue.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "blue" "-")
((triple2) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Gary is young.
True
4
proof
[(((((triple6) -> rule5) triple6) -> rule3))]
("Gary" "is" "young" "+")
((((triple6) -> (rule5 % int2)) triple6) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not young.
False
4
inv-proof
[(((((triple6) -> rule5) triple6) -> rule3))]
("Gary" "is" "young" "-")
((((triple6) -> (rule5 % int2)) triple6) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not kind.
True
6
proof
[(((triple7 ((((triple6) -> rule5) triple6) -> rule3)) -> rule4) OR ((((triple6) -> rule6) ((((triple6) -> rule5) triple6) -> rule3)) -> rule4))]
("Gary" "is" "kind" "-")
((triple7 ((((triple6) -> (rule5 % int3)) triple6) -> (rule3 % int2))) -> (rule4 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((triple6) -> (rule6 % int4)) ((((triple6) -> (rule5 % int3)) triple6) -> (rule3 % int2))) -> (rule4 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is kind.
False
6
inv-proof
[(((triple7 ((((triple6) -> rule5) triple6) -> rule3)) -> rule4) OR ((((triple6) -> rule6) ((((triple6) -> rule5) triple6) -> rule3)) -> rule4))]
("Gary" "is" "kind" "+")
((triple7 ((((triple6) -> (rule5 % int3)) triple6) -> (rule3 % int2))) -> (rule4 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((triple6) -> (rule6 % int4)) ((((triple6) -> (rule5 % int3)) triple6) -> (rule3 % int2))) -> (rule4 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Fiona is not rough.
Unknown
inv-rconc
[@3: Fiona is rough.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule5 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is blue.
Unknown
rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not round.
Unknown
inv-rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is young.
Unknown
rconc
[@3: Fiona is young.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule2 <- FAIL)]]
("Fiona" "is" "young" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is rough.[(triple1 OR ((((triple2) -> rule2)) -> rule6))] Bob is round.[(triple2)] Bob is young.[(triple3 OR ((triple2 ((triple2) -> rule2)) -> rule3))] Fiona is not cold.[(triple4)] Fiona is quiet.[(triple5)] Gary is blue.[(triple6)] Gary is rough.[(triple7 OR ((triple6) -> rule6))] @1: Bob is blue.[(((triple2) -> rule2))] Bob is not kind.[(((triple1 triple3) -> rule4) OR ((triple1 ((triple2 ((triple2) -> rule2)) -> rule3)) -> rule4) OR ((((((triple2) -> rule2)) -> rule6) triple3) -> rule4) OR ((((((triple2) -> rule2)) -> rule6) ((triple2 ((triple2) -> rule2)) -> rule3)) -> rule4))] Gary is round.[(((triple6) -> rule5))] @2: Gary is young.[(((((triple6) -> rule5) triple6) -> rule3))] @3: Gary is not kind.[(((triple7 ((((triple6) -> rule5) triple6) -> rule3)) -> rule4) OR ((((triple6) -> rule6) ((((triple6) -> rule5) triple6) -> rule3)) -> rule4))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
((triple6) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not kind.
("Bob" "is" "kind" "-")
((triple1 triple3) -> (rule4 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
((triple1 ((triple2 ((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2)) triple3) -> (rule4 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((triple2) -> (rule2 % int4))) -> (rule6 % int3)) ((triple2 ((triple2) -> (rule2 % int4))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Gary is round.
("Gary" "is" "round" "+")
((triple6) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple6) -> (rule5 % int2)) triple6) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not kind.
("Gary" "is" "kind" "-")
((triple7 ((((triple6) -> (rule5 % int3)) triple6) -> (rule3 % int2))) -> (rule4 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((triple6) -> (rule6 % int4)) ((((triple6) -> (rule5 % int3)) triple6) -> (rule3 % int2))) -> (rule4 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4