Bob is smart. Bob is young. Charlie is cold. Charlie is not nice. Gary is cold. Gary is smart. Gary is young. Smart people are round. If someone is round then they are quiet. Smart, nice people are quiet. All cold people are smart. If someone is quiet and cold then they are smart. Young people are blue.
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Smart, nice people are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
All cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If someone is quiet and cold then they are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Bob is smart.
True
1
proof
[(triple1)]
("Bob" "is" "smart" "+")
triple1
Gary is not young.
False
1
inv-proof
[(triple7)]
("Gary" "is" "young" "-")
triple7
Gary is blue.
True
2
proof
[(((triple7) -> rule6))]
("Gary" "is" "blue" "+")
((triple7) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple2) -> rule6))]
("Bob" "is" "blue" "-")
((triple2) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule2) OR ((((((triple5) -> rule4)) -> rule1)) -> rule2))]
("Gary" "is" "quiet" "-")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((((triple5) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Charlie is quiet.
True
4
proof
[(((((((triple3) -> rule4)) -> rule1)) -> rule2))]
("Charlie" "is" "quiet" "+")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not quiet.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule1)) -> rule2))]
("Charlie" "is" "quiet" "-")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "blue" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is smart.[(triple1)] Bob is young.[(triple2)] Charlie is cold.[(triple3)] Charlie is not nice.[(triple4)] Gary is cold.[(triple5)] Gary is smart.[(triple6 OR ((triple5) -> rule4))] Gary is young.[(triple7)] @1: Bob is blue.[(((triple2) -> rule6))] Bob is round.[(((triple1) -> rule1))] Charlie is smart.[(((triple3) -> rule4))] Gary is blue.[(((triple7) -> rule6))] Gary is round.[(((triple6) -> rule1) OR ((((triple5) -> rule4)) -> rule1))] @2: Bob is quiet.[(((((triple1) -> rule1)) -> rule2))] Charlie is round.[(((((triple3) -> rule4)) -> rule1))] Gary is quiet.[(((((triple6) -> rule1)) -> rule2) OR ((((((triple5) -> rule4)) -> rule1)) -> rule2))] @3: Charlie is quiet.[(((((((triple3) -> rule4)) -> rule1)) -> rule2))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
((triple5) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple7
Bob is blue.
("Bob" "is" "blue" "+")
((triple2) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple3) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple7) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple6) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((((triple5) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3