Bob is smart. Charlie is round. Charlie is smart. Dave is green. Dave is round. Dave is smart. Dave is white. Dave is young. Gary is round. Gary is young. All round people are smart. All white people are round. If someone is young then they are cold. Young, furry people are green. All young, smart people are green. If someone is young and not round then they are furry. All round, young people are furry. If Gary is not smart then Gary is not cold.
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
All round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
All white people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If someone is young then they are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Young, furry people are green.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
All young, smart people are green.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is young and not round then they are furry.
((("someone" "is" "young" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "furry" "+"))
All round, young people are furry.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If Gary is not smart then Gary is not cold.
((("Gary" "is" "smart" "~")) -> ("Gary" "is" "cold" "-"))
Dave is young.
True
1
proof
[(triple8)]
("Dave" "is" "young" "+")
triple8
Dave is not green.
False
1
inv-proof
[(triple4 OR ((triple8 triple6) -> rule5) OR ((triple8 ((triple5) -> rule1)) -> rule5) OR ((triple8 ((triple5 triple8) -> rule7)) -> rule4) OR ((triple8 ((((triple7) -> rule2)) -> rule1)) -> rule5) OR ((triple8 ((((triple7) -> rule2) triple8) -> rule7)) -> rule4))]
("Dave" "is" "green" "-")
triple4
((triple8 triple6) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple8 ((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((triple8 ((triple5 triple8) -> (rule7 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((triple8 ((((triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((triple8 ((((triple7) -> (rule2 % int3)) triple8) -> (rule7 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is cold.
True
2
proof
[(((triple8) -> rule3))]
("Dave" "is" "cold" "+")
((triple8) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple10) -> rule3))]
("Gary" "is" "cold" "-")
((triple10) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "cold" "-")
Charlie is furry.
Unknown
rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Bob is smart.[(triple1)] Charlie is round.[(triple2)] Charlie is smart.[(triple3 OR ((triple2) -> rule1))] Dave is green.[(triple4 OR ((triple8 triple6) -> rule5) OR ((triple8 ((triple5) -> rule1)) -> rule5) OR ((triple8 ((triple5 triple8) -> rule7)) -> rule4) OR ((triple8 ((((triple7) -> rule2)) -> rule1)) -> rule5) OR ((triple8 ((((triple7) -> rule2) triple8) -> rule7)) -> rule4))] Dave is round.[(triple5 OR ((triple7) -> rule2))] Dave is smart.[(triple6 OR ((triple5) -> rule1) OR ((((triple7) -> rule2)) -> rule1))] Dave is white.[(triple7)] Dave is young.[(triple8)] Gary is round.[(triple9)] Gary is young.[(triple10)] @1: Dave is cold.[(((triple8) -> rule3))] Dave is furry.[(((triple5 triple8) -> rule7) OR ((((triple7) -> rule2) triple8) -> rule7))] Gary is cold.[(((triple10) -> rule3))] Gary is furry.[(((triple9 triple10) -> rule7))] Gary is smart.[(((triple9) -> rule1))] @2: Gary is green.[(((triple10 ((triple9) -> rule1)) -> rule5) OR ((triple10 ((triple9 triple10) -> rule7)) -> rule4))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
((triple2) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple4
((triple8 triple6) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple8 ((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((triple8 ((triple5 triple8) -> (rule7 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((triple8 ((((triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((triple8 ((((triple7) -> (rule2 % int3)) triple8) -> (rule7 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
triple5
((triple7) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple6
((triple5) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Dave is cold.
("Dave" "is" "cold" "+")
((triple8) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple5 triple8) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple7) -> (rule2 % int2)) triple8) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((triple10) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple9 triple10) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple9) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple10 ((triple9) -> (rule1 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((triple10 ((triple9 triple10) -> (rule7 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2