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