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