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