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