Bob is furry. Bob is nice. Bob is smart. Bob is young. Charlie is blue. Charlie is nice. Erin is nice. Gary is blue. Gary is smart. Gary is young. Furry things are cold. All nice things are round. All round things are smart.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
All nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
All round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
Bob is young.
True
1
proof
[(triple4)]
("Bob" "is" "young" "+")
triple4
Gary is not young.
False
1
inv-proof
[(triple10)]
("Gary" "is" "young" "-")
triple10
Bob is round.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "round" "+")
((triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple6) -> rule2))]
("Charlie" "is" "round" "-")
((triple6) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
True
3
proof
[(((((triple6) -> rule2)) -> rule3))]
("Charlie" "is" "smart" "+")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Erin is not smart.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule3))]
("Erin" "is" "smart" "-")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "cold" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "cold" "+")
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Bob is furry.[(triple1)] Bob is nice.[(triple2)] Bob is smart.[(triple3 OR ((((triple2) -> rule2)) -> rule3))] Bob is young.[(triple4)] Charlie is blue.[(triple5)] Charlie is nice.[(triple6)] Erin is nice.[(triple7)] Gary is blue.[(triple8)] Gary is smart.[(triple9)] Gary is young.[(triple10)] @1: Bob is cold.[(((triple1) -> rule1))] Bob is round.[(((triple2) -> rule2))] Charlie is round.[(((triple6) -> rule2))] Erin is round.[(((triple7) -> rule2))] @2: Charlie is smart.[(((((triple6) -> rule2)) -> rule3))] Erin is smart.[(((((triple7) -> rule2)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple6) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple7) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2